|
这一章主要讨论一阶谓词逻辑描述下的归结（resolution）推理方法，它是一种机械化的可在计算机上加以实现的推理方法。引人注目的人工智能程序设计语言Prolog，就是基于归结原理的一种逻辑程序设计语言。
我们首先介绍命题逻辑下的归结方法，可使读者对归结过程一目了然。进而给出由Herbrand 定理描述的一阶逻辑的半可判定算法，接着介绍本章的中心内容�D�D归结方法，最后讨论几种非归结方法。
2.1 命题逻辑的归结法
设有由命题逻辑描述的命题
,
,
和B，要求来证明在∧∧→B定理（重言式），这就是我们的问题。如何建立推理规则，来证明这个定理是我们的任务。很显然，
∧∧∧→B是重言式等价于∧∧∧～B
是矛盾（永假）式。归结推理方法就是从∧∧∧～B出发，使用归结推理来寻找矛盾，最后证明定理∧∧→B的成立。这种方法可称作反演推理方法。
2.1.1 建立子句集
为使用归结方法，首先要把
∧∧～B化成一种称作子句形的标准形式，对命题公式∧∧～B来说，其子句形式就是合取范式。如：P∧(Q∨R)∧(～P∨～ Q)∧( P∨～Q∨R)
然后将这合取范式写成集合的表示形式，这只是为了说明上的方便。得
S＝{P，Q∨R，～P∨～Q,P∨～Q∨R}。
合取范式与S不同的仅是∧以，代替了。
称S中的每个元素为一个子句，P，Q∨R，～P∨～Q，P∨～Q∨R 都是子句。而S称为对应于
∧∧～B
的子句集。2.1.2 归结式
设有两个子句
＝P∨'
=
～P∨'从中消去互补对，所得的新子句
R(
，)＝C∨C
便称作子句C1，C2的归结式。没有互补对的两子句没有归结式。
归结推理规则就指的是对两子句做归结，也即求归结式。
为了说明归结推理规则是正确的，必须证明
∧TR(，)也即归结式是原两子句的逻辑推论，或说任一使
,为真的解释I下必有R(，)也为真。这是容易证明的。设I是使
、为真的任一解释，若I下的P为真，从而～P为假，必有I下C
为真，故I下R(，)为真。若不然，在I下P为假，从而I下C
为真，故I下R(，)为真。于是∧TR(，)成立。当
=P=P→Q=～P∨Q有R(
，)＝Q这实际上是假言推理P∧(P→Q)TQ。这样说来归结推理规则是假言推理的推广。
当
＝P＝～P这两个子句的归结式为空，记作□称作空子句。显然
，
同时成立便是矛盾，或说空子句□体现了矛盾。2.1.3 归结推理过程
从子句集S出发，仅只对S的子句间使用归结推理规则，并将所得归结式仍放入S中，进而再对新子句集使用归结推理规则，重复这些步骤直到得到空子句□。便说明S是不可满足的，从而与S对应的定理A1∧A2∧A3→B是成立的。
因为归结推理规则是正确的推理规则，归结式是原两子句的逻辑推论，于是归结过程出空子句□，说明S中必有矛盾。
 |
例： |
| 证明 (P→Q)∧～Q～P 先将 (P→Q) ∧～Q ∧～(～P) 化成合取范式，得 (～P∨ Q) ∧ ～Q ∧ P 建立子句集 S={ ～P∨ Q，～Q，P} 对S做归结 ⑴ ～P∨ Q ⑵ ～Q ⑶ P ⑷ ～P (1)(2)归结 ⑸ □ (3)(4)归结 证毕。 |
一阶谓词逻辑的归结方法比命题逻辑的归结法要复杂多，原因是要对量词和变量做专门处理，从2.2 节开始讨论。