定理機器證明

用計算機自動地進行推理和證明定理。所謂定理，並不限於數學的，凡是用演繹法推導的論斷都可以看作是定理。定理證明是人工智慧研究中的一個基本課題，廣泛應用於各種人工智慧系統，例如問題求解系統、答問系統、自動程序設計、自動情報檢索和各種數學系統。

①歸結方法：歸結是定理機器證明的一個重要方法，1965年由J.A.魯賓遜建立。例如以P、Q、R、S分別代表四種陳述，-P表示P不真,P∨Q表示P和Q至少有一個為真。最簡單的歸結原理就是：由P∨Q和-P∨R可推出Q∨R。假定已知事實：-P∨-Q、Q∨R∨-S、P、S,欲證R成立。歸結方法總是使用反證法，因此，假定要證的定理不成立，即假定-R。把P-∨-Q和Q∨R∨-S相歸結得-P∨R∨-S,以此與-R歸結得-P∨-S，再與P歸結得-S,結果與S矛盾，故定理得證。

②自然推導：歸結方法及其改進過於一般化，故效率不高。人在某一領域內證明定理是用自然推導法，即除一般的邏輯推導外還利用他在這一領域中的知識和經驗。模仿人的這種自然推導法的最初成果是1963年A.紐厄爾、J.C.肖和H.A.西蒙的LT系統。另外，還有以歸結方法與自然推導相結合的系統。

③判定方法：在較小的領域內找一個有效的判定方法來作定理證明也受到人們的重視。這方面最早的工作是A.塔斯基的初等代數和初等幾何的判定方法。這種方法雖效率很低，但後來又有人作了不少改進。王浩給出命題邏輯的一個很有效的判定方法。吳文俊提出的關於初等幾何和微分幾何的判定方法也是很成功的。

參考書目

C. Chang　and　R. C. Lee, Symbolic　Logic　and Mechanical　Theorem　Proving, Academic Press,New York,1973.