自動定理證明是人工智慧研究領域中的一個非常重要的課題，其任務是對數學中提出的定理或猜想尋找一種證明或反證的方法。因此，智慧型系統不僅需要具有根據假設進行演繹的能力，而且也需要一定的判定技巧。
基本介紹
- 中文名：自動定理證明
- 套用：人工智慧
發展歷史,證明系統,模型,證明技術,歸結定理證明,Horn子句實現超級歸結,
發展歷史
1956年，Newell，Shaw和Simon給出了一個稱為“邏輯機器”的程式，證明了羅素、懷德海所著《數學原理》中的許多定理，這標誌著自動定理證明的開端。
1959年，Gelernter給出了一個稱為“幾何機器”的程式,能夠做一些中學的幾何題，速度與學生相當。
1960年,美籍華裔王浩在IBM704上,編程實現了三個程式，第一個程式用於命題邏輯，第二個程式讓機器從基本符號出發自動生成合適命題邏輯公式並選出其中定理，第三個程式用於判定一階邏輯中的定理。他證明了羅素、懷德海《數學原理》中的幾乎所有定理。他的方法人們稱之為“王浩”算法。他的這項工作在1984年首屆自動定理證明大會上獲最高獎—“里程碑”獎。
1960年，Davis、Putnan等給出了D一P過程，大大簡化了命題邏輯的處理。
1965年，Robinson提出一歸結方法，使得自動定理證明領域發生了質的變化。
1968年，蘇聯Maslov提出了逆向法，是蘇聯人六、七十年代在該領域做的主要工作。
歸結方法有許多重要改進，每種改進有各自的優點。語義歸結由Slagle提出，它將超歸結(Robinson)、換名
歸結(Meltzer)、支架集策略(Wos，RobinSon)等方法一體化。鎖歸結，由Boyer在1971年提出，是一個很高效的規則。線性歸結由Loveland和Luckham在1970年獨立提出。
證明系統
用謂詞演算公式描述的事實即證明系統中的公理(axioms)。證明系統(proof system)是套用公理演繹出定理(theorems)的合法演繹規則的集合。所謂演繹，也叫歸約(deduction)，是對證明系統中合法推理規則的一次套用。在一個簡單的演繹步驟中，可以從公理導出結論(conclusion)，中間可以利用這些規則演繹出的定理。
證明(proof)是個語句序列，以每個語句得到證明而結束，即每個句子要么演繹成公理，要么演繹成前此導出的定理。一個證明若有N個語句(命題)則稱N步證明，反駁(refutation)是一個語句的反向證明。它證明一個語句是矛盾的，即不合乎給定的公理。
同一命題的正向證明和反駁有時會有天壤之別，證明長度和複雜性差別很大。構造一個證明或反駁要有深入的洞察、聯想，還要有點靈感。
一個語句若能從公理出發推演出來，則稱合法語句。任何合法語句也叫做定理(theorem)。從某一公理集合導出的所有定理集合稱為理論(theory)。一般說來,理論具有一致性，它不包含相互矛盾的定理。
模型
從公理集合中導出定理集稱之為理論。有了理論要解釋它的語義必須藉助某個模型(model)。因為形式系統只是符號抽象，藉助模型可為每個常量、函式、謂詞符號找到真理性的解釋，即定義每個論域，並表明域上成員和常量公理之間的關係。公理的謂詞符號必須派定為域中對象的性質，函式派定為對域中對象的操作。不一致的理論就沒有模型，因為無法找到同時滿足相互矛盾定理的解釋。
公理集合一般情況下只是定義的部分(偏)函式和謂詞，是問題域的一個側面。所以能滿足該理論的模型往往不止一個。
證明技術
謂詞演算具有完整性，理論上可做出自動生成程式,並證明按公理集合建立的任何理論。它們是公理集合的邏輯結論。但實際做起來，要找到切題的證明如同大海撈針，效率難以容忍。
即使把問題限制在證明單個命題，關鍵仍然是效率。如果從公理出發做出每一個步驟，在新的步驟上仍然要查找每一個公理找出可能的推理。如此下去就形成一個龐大的樹行公理集，每層的節點都是表示一個公理的語句，其深度和寬度隨問題和最初給出的公理而定，一層一步驟，N層的樹就是N步推理。
歸結定理證明
歸結法是命題演算中對合適公式的一種證明方法。為了證明合適公式F為真，歸結法證明￢F恆假來代替F永真。歸結原理是：設有前題L∨P和￢L∨R則其邏輯結論是P∨R，因為兩個子句中含有一個命題的正逆命題(L,￢L)。若L為真￢L一定為假，P若為真，P∨R也為真。若L為假，￢L為真，P若為真，P∨R也為真。這個推理把兩子句合一(unification)並消去一對正逆命題，故歸結，也譯做消解。歸結證明的過程稱為歸結演繹。其步驟如下：
[1]把前題中所有命題換成子句形式。
[2]取結論的反，並轉換成子句形式加入[1]中的子句集。
[3]在子句集中選擇含有互逆命題的命題歸結。用合一算法得出新子句(歸結式)再加入到子句集。
[4]重複[3]，若歸結式為空則表示此次證明的邏輯結論是矛盾，原待證結論若不取反則恆真，命題得證，否則繼續重複[3]。
Horn子句實現超級歸結
Horn子句是至多只有一個非負謂詞符號的子句。這就等於通過謂詞演算一個語句只包含一個蘊含運算符連線前題和結論，前題是由‘∧’連線的幾個謂詞，結論就是單一的謂詞符號。
Horn子句形式示例如下:
￢P∨ ￢Q∨S∨ ￢R∨ ￢T（1）
其中只有一個非負謂詞S，可作以下演算，先將S移向右方
┠S∨￢P∨￢Q∨ ￢R∨ ￢T （2）
按德·摩根定律
┠ S∨￢ (P∧Q∧R∧T) （3）
‘∨￢’即‘→’，則
┠S←(P∧ Q∧ R∧ T) （4）
此即條件Horn子句，因為式(4)的意義是if(P∧Q∧R∧T)then S。顯然,若S為空，則為無條件Horn子句是一個斷言(事實)。
超級歸結實質上是將無條件Horn子句中的謂詞符號和條件子句中的對應謂詞符號合一。找出所有子句中變數的實例集，使每一條件子句為真。如果不滿足，則尋找新的實例(回溯算法)，如果滿足了也要找出所有實例。
為了消去不必要的匹配以提高超級歸結的效率，cut操作是必須的。它可以由程式設計師指定。當找到一個解之後不再搜尋其他解。它本身是個無變元謂詞，當執行到它時不再回溯。
