自動推理

在20世紀60年代中期以前，定理機器證明的注意力還僅僅限於數學方面。

從60年代後期，開始將注意力轉向數學以外的其他領域，如程序自動生成、邏輯程序設計以及更一般的智能系統中的推理問題。定理機器證明的研究是自動推理領域中的先驅性工作。

70年代專家系統和知識工程的出現，使人們認識到，僅僅研究從真前提得出真結果的古典推理方法是不夠的，因為人類面對的是一個充滿不確定信息的環境，人類在這種環境裏進行着有效的思考和推理。

為了建立類似於人的智能系統，研究更接近人類思維方式的推理，如非單調推理、模糊推理等，變得越來越必要。

自動推理的研究，一方面表現在專家系統中，各種面向特殊問題的推理方式的研究，例如，DENDRAL的用於化學合成的推理，PROSPECTOR的用於地質方面的推理，MYCIN的用於醫療診斷的推理等；另一方面，在計算機輔助推理的研究上也取得成果，回答了以前在數學和形式邏輯方面的一些未解問題。隨之而來的，面向自動推理的邏輯程序設計語言（如PROLOG）也引起了研究者的興趣。

自動推理的研究內容有模型生成與定理機器證明、程序正確性驗證、邏輯程序設計、常識推理、非單調推理、模糊推理、約束推理、定性推理、類比推理、歸納推理、自然演繹法、歸結方法、重寫方法、吳方法等。自動推理的近期目標是得到各種推理程序，它們中的每一個都相當於一個自動推理助手，人們能有效地和這個助手“交談”。遠期目標是當你向這樣一個程序提出問題後，你就可以去考慮別的問題了；當你再回來時，原來的問題已經解決了。 ^[1]