機器定理證明

機器定理證明是人工智能的重要研究領域，它的成果可應用於問題求解、自然語言理解、程序驗證和自動程序設計等方面。數學定理證明的過程儘管每一步都很嚴格有據，但決定採取什麼樣的證明步驟，卻依賴於經驗、直覺、想象力和洞察力，需要人的智能。因此，數學定理的機器證明和其他類型的問題求解,就成為人工智能研究的起點。早在17世紀中葉，萊布尼茲就提出過用機器實現定理證明的思想。19世紀後期G.弗雷格的“思想語言”的形式系統，即後來的謂詞演算，奠定了符號邏輯的基礎，為自動演繹推理提供了必要的理論工具。20世紀50年代，由於數理邏輯的發展,特別是電子計算機的產生和應用,機器定理證明才變為現實。A.紐厄爾和H.A.西蒙首先用探試法實現了用以證明命題邏輯中重言式的邏輯理論家系統LT。後來，開始探討通用的機器定理證明的方法，歸結原理是其中突出的例子。

歸結原理和非歸結定理證明一階謂詞邏輯的恆真性問題是不可解的，即不存在能判定一階邏輯中任意合式公式是不是恆真式的算法，但是這個問題又是部分可解的。如果A是恆真式,那麼必有算法可以證明。許多一階邏輯的證明算法都以J.厄爾布朗定理為基礎，其中以1965年J.A.魯賓遜提出的、對於一階邏輯是完備的證明算法即歸結原理最為著名。歸結原理的提出，把機器定理證明的研究推向高潮。但歸結原理不依賴於領域知識，不使用依賴問題領域的探試法，證明過程冗長，不能在合理的時間和計算機存儲容量內證明較為複雜的數學定理，因此人們又提出非歸結定理證明方法，後來又對以探試法為基礎的問題求解技術發生興趣。與此同時還出現了因否定歸結原理進而否定所有自動演繹方法的傾向。但是人工智能所要解決的問題，其信息往往是不完全的，而且即使信息完全，要對有限的但為數眾多的情形一一列舉,實際上也不可行,因而只有用演繹推理的方法。邏輯程序設計和日本以PROLOG為原型開發第五代計算機系統的核語言，進一步恢復了歸結原理和自動演繹技術的地位。人工智能的歷史表明，以認知心理學為基礎的探試法和以邏輯為基礎的自動演繹相輔相成，不可偏廢。自動演繹與探試法等技術相結合而不用歸結原理的定理證明技術，主要用於數學定理的機器證明。

幾何定理的機器證明在數學定理機器證明中，有一類問題已有判定算法，如1951年W.斯米列夫給出的阿貝爾羣判定算法，1951年A.塔斯基給出的初等幾何和代數的判定算法，1960年王浩提出的命題邏輯判定算法和1976年以來吳文俊提出的初等幾何和微分幾何定理機器證明的理論和方法。

非標準邏輯中的自動演繹以經典的一階邏輯為基礎的自動演繹技術比較成熟。為了適應人工智能中複雜的推理形式，需要研究高階邏輯和非標準邏輯中的自動演繹技術並從實用角度將這類邏輯表示形式轉換成等價的經典一階邏輯的表示形式。

邏輯程序設計將一階謂詞演算的子集直接作為程序設計語言的技術和方法。PROLOG語言是初步實現邏輯程序設計基本思想的第一個語言，R.科瓦爾斯基則曾對HORN子句作了過程性解釋，系統地闡明瞭邏輯程序設計的基本理論。