定理機器證明是用計算機自動地進行推理和證明數學定理。又稱為自動定理證明(ATP)。讓機器去證明數學定理的想法，在17世紀G.W.Leibniz 創立數理邏輯時就產生了，但這一想法的真正實現，是在20世紀40年代計算機誕生以後。
基本介紹
- 中文名：定理機器證明
- 外文名：mechanical theorem proving
- 機器：計算機
- 套用：各種人工智慧系統
- 作用：推理和證明定理
簡介,方法舉例,
簡介
從1956年A.Newell，J.C.Shaw,H.A.Simon發表他們的著名論文“邏輯理論機”算起，自動定理證明這個研究領域已經有近四十年的歷史了。邏輯理論機是機械地模仿人類在證明命題邏輯定理時所用的推導過程。1959年 H.Gelernter 等人做出了幾何定理證明機(GTM)。GTM能夠證明直線圖形中的大部分高中的考試題，而且運行時間也常常與高中學生做題的時間相當。1959年P.C.Gilmore設計了關於謂詞演算的機械證明程式。在1958到1960年間王浩研究出關於命題演算和謂詞演算的機械證明程式。1965年J.A.Robinson提出了歸結原理。歸結原理實質上是一條簡潔的推理規則。使用這一條規則，對一階邏輯中的任一個恆真公式，都將是可證的。L.Wos是最成功地實現歸結系統的研究者之一，為此，他獲得首次ATP獎。1972年左右，以L.Wos 為首的集體建立了一個以歸結方法為主的自動推理系統AURA。這個系統對於解有限數學，線路設計，程式正確性驗證及形式邏輯等領域中的疑難問題，提供了幫助。歸結方法是ATP領域中第一類方法———邏輯方法的代表。
ATP領域中第二類方法———類人方法，有時也稱為自然演繹或自然推導法。A.Newell等人的邏輯理論機就使用了類人方法。1966年美國麻省理工學院的L.Norton建造了一個系統ADEPT，該系統是一個關於群論的啟發式定理證明系統，它使用了很多有效的啟發式規則。這個系統的能力界限是能夠證明：若
，則群是交換群。
ATP領域中的第三類方法是所謂判定過程。判定過程是指: 判斷一個理論中的某個公式的有效性。1978年，中國的吳文俊關於平面幾何和微分幾何的定理機 器證明方法(亦即吳方法) 被認為是ATP領域中判定方法的一個最好的結果。使用這個方法，在計算機上證明和發現了平面幾何中一些有趣的定理。
下面用簡單而直觀的例子說明ATP領域中這三類方法。我們知道一個定理：若A成立，則B成立;還知道一個事實：A成立。欲證明一個結論：B也成立。我們想做的事，在數理邏輯中 ,相當於去證明公式：
(1)
是一個定理，亦即證明公式(1)是恆真的。
第一種方法：歸結方法是反駁方法，要證明公式(1)是恆真的，相當於證明公式(1)的否定是恆假的，亦即證明：
(2)
是恆假的(～B表示B的否定)。A和(A→B)歸結得B，B和～B歸結得恆假公式(即空子句)。因此，公式(2)是恆假的，所以公式(1)是恆真的，定理得證。
第二種方法：類人方法就是模仿人在證明定理時的思維過程，將原目標不斷分解成易證的子目標，直到子目標都是(P→P)的形式。為了證 明公式(1)，只要能證明(A→ B)或者(( A→ B)→B)中的一個即可 (這稱為自然演繹法中的“或分枝規則”)。(A→B)無法證明，考慮：
(3)
只要能證明(B→ B)和A即可(這稱為“反向鏈規則”)。而(B→ B)可證，下面證明A使用定理(1)的前提，即是要證明：
(4)
對公式(4)再使用“或分枝規則”，只要能證明(A→A)或者((A→B)→A)中的一個即可，而(A→ A)可證，故式(4)可證，因此A可證，故式(3)可證，所以定理(1)可證。
第三種方法：判定方法不是直接去證明定理，而是去判定這個定理是否正確，對定理使用真值表法即可判定它是成立的。
上述三種方法較詳細的論述可分別參見歸結方法，自然演繹法，吳方法。
定理機器證明面對的是數學領域，這就決定了定理機器證明必然要面臨巨大的困難。因此，從20世紀80年代開始，很多研究定理機器證明的學者，轉向了使用簡單推理就能獲得成效的領域，從而誕生了人工智慧中一個極為活躍的研究領域———自動推理。自動定理證明和自動推理在人工智慧領域中越來越顯出其重要性。
方法舉例
①歸結方法：歸結是定理機器證明的一個重要方法，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.塔斯基的初等代數和初等幾何的判定方法。這種方法雖效率很低，但後來又有人作了不少改進。王浩給出命題邏輯的一個很有效的判定方法。吳文俊提出的關於初等幾何和微分幾何的判定方法也是很成功的。
