基本介紹
- 中文名：非歸結定理證明
- 闡述：一種機器定理證明技術
- 類別：相關辭彙
- 相關：歸結原理
作用,重要例子,參考書目,
作用
不用歸結原理而用自然演繹技術與探試策略等相結合的一種機器定理證明技術。
為了提高歸結證明過程的效率，曾提出各種改進方案。另一條途徑是在定理的機器證明中不用歸結原理而用歷史上早已形成的自然推理或稱自然演繹技術，但在其中引入問題所需的特定探試策略。這就是1977年W.W.布萊塞提出的所謂非歸結定理證明的基本思想。作為這種思想的具體體現，曾研製出一個運用探試策略的新的自然演繹系統IMPLY。R.S.鮑耶和 J.S.莫爾的數學歸納法機械定理證明系統也是成功地運用探試策略的一個重要例子。
重要例子
自然演繹系統由一組公理和一套推理規則組成，每條推理規則將若干恆真式映射為一個恆真式。如果存在一個恆真式系列，使得序列中每一恆真式或者是一公理，或者是一定理（即可從序列中位於其前的恆真式根據推理規則導出），則序列中最後一項恆真式稱為在該推理系統中可導出（或可證明）。一階邏輯的推理系統是完備的，也就是每一恆真式都可從該系統中導出。如果推理系統的公理和推理規則比較豐富，使得每一恆真式的導出過程都很自然，符合人的思維習慣，這樣的推理系統稱為自然推理系統或自然演繹系統。根據數理邏輯中著名的哥德爾定理，對於二階邏輯不存在完備的演繹系統。採用不同的公理、推理規則，便可得到不同的自然演繹系統。著名的根岑系統便是20世紀30年代提出的典型的自然演繹系統。自然演繹系統的顯著特點是在證題全過程中，始終維持前提和結論的明確界限。例如在下例的推理圖式中，橫線以上的H1、H2、H3是前提。
橫線以下的C1，C2則是有待證明的結論。由H1，H2可推出C1（根據充分條件的假言推理原則），又根據H3和已推出的C1可推出C2。同樣的例子如運用歸結原理，其子句集可表示為
1P
2 塡P∨Q
3 塡R∨-Q∨S
4 塡Q∨S
5 塡Q∨塡S
此時由於採用反證法，將結論的否定式併入子句集，不區分前提與結論，有關的推理信息便已喪失。自然演繹的優點是推理過程自然易懂，有利於發揮人機互動作用，便於引用探試策略。缺點是要用許多條複雜的推理規則。而運用歸結原理，雖然推理過程不易控制，但只需要一條推理規則。因此，自然演繹與歸結原理的優缺點是相比較而存在的，具有相對的意義，不能絕對化。
參考書目
W.W.Bledsoe，Non-resolutiontheoremProving，Artificial Intelligence, North-Holl and Publ.Co., Amsterdam,1977.
Zohor Manna,Mathematical Theory of computation, McGraw-Hill,New York,1974.
R.S.Boyer and J.S.Moore, A Computational Logic, Academic Press,New York,1979.
