4.2归结（消解Resolution）

　　1．归结原理
　　归结原理是一种定理证明方法，1965年由Robinson提出。由于该方法简单，容易在计算机上程序实现，因此一经提出，就得到了人们的广泛关注，对自动定理证明的研究起到了很大的推动作用。
　　用归结原理证明定理有些类似于"反证法"的思想。在反证法中首先假定要证明的结论不成立，然后通过推导出存在矛盾的方法，反证出结论成立。在归结法中首先对结论求反，然后将已知条件和结论的否定合在一起用子句集表达。如果该子句集存在矛盾，则证明了结论的正确性。如何证明子句集存在矛盾呢？其思路如下：
　　设S是已知条件和结论的否定合并后所对应的子句集。假定有一种变换方法，可以对S实施一系列的变换。而且该变换能够保证变换前后的子句集，在不可满足的意义下是等价的。这样，如果最终得到的子句集是不可满足的，就证明了子句集S是不可满足的，从而证明结论成立。
　　由前面合适公式转化为子句集的过程可知，子句集中的子句是"与"的关系，如果在子句集中出现了空子句，则说明该子句集是不可满足的。因此，归结过程就是"寻找"空子句的过程。如果把这一过程看作是搜索的话，初始状态就是已知条件和结论的否定对应的子句集，而目标就是空子句，规则就是归结。

　　在定理证明系统中，已知一公式集F1，F2，…，Fn，要证明一个公式W（定理）是否成立，即要证明W是公式集的逻辑推论时，一种证明法就是要证明F1∧F2∧…∧Fn→W为永真式。如果直接应用推理规则进行推导，则由于演绎技巧等因素的影响，给建立机器证明系统带来困难。另一种证明法是采用间接法（反证法），即不去证明F1∧F2∧…∧Fn→W为永真，而是去证明F＝F1∧F2∧…∧Fn∧~W为永假，这等价于证明F对应的子句集S＝S0∪{~W}为不可满足的。这时如果用归结作为推理规则使用时，就可以使机器证明大为简化。
　　归结原理的基本思路是设法检验扩充的子句集Si是否含有空子句，若S集中存在空子句，则表明S为不可满足的。若没有空子句，则就进一步用归结法从S导出S1，然后再检验S1是否有空子句。可以证明用归结法导出的扩大子句集S1，其不可满足性是不变的，所以若S1中有空子句，也就证得了S的不可满足性。归结过程可以一直进行下去，这就是要通过归结过程演绎出S的不可满足性来，从而使定理得到证明。下面就来讨论归结过程是怎样进行的。

　　2．命题逻辑的归结原理
　　命题逻辑，简单的说，就是不含有变量的逻辑。命题逻辑的归结方法比较简单，首先介绍命题逻辑的归结原理及方法。

　　（1）归结式（或预解式）的定义及性质
归结式：对任意两个子句C1和C2，若C1中有一个文字L1，而C2中有一个与L1成互补的文字L2，则分别从C1、C2中删去L1和L2，并将其剩余部分组成新的析取式，则称这个新子句为归结式或预解式。

这里的"□"表示"空"的意思，有时用NIL表示。如果子句集中出现了"空"，则表示该子句集存在矛盾，是不可满足的。

例：设两个子句C1＝L∨C1′，C2＝（~L）∨C2′，则归结式C＝C1′∨C2′。当C1′＝C2′＝□时，C＝□。
定理：二个子句C1和C2的归结式C是C1和C2的逻辑推论。
证：设C1＝L∨C1′，C2＝（~L）∨C2′关于解释I为真，则需证明C＝C1′∨C2′关于解释I也为真。
关于解释I，L和~L二者中必有一个为假。若L为假，则C1′必为真，否则C1为假，这与前提假设矛盾，所以只能是C1′为真。
同理，若~L为假，则C2′必为真。最后有C＝C1′∨C2′关于解释I为真，即C是C1和C2的逻辑推论。[证毕]
推论：子句集S＝{C1，C2，…，Cn}与子句集S1＝{C，C1，C2，…，Cn}的不可满足性是等价的（S1中C是C1和C2的归结式，即S1是对S应用归结法后导出的子句集）。
证：设S是不可满足的，则C1，C2，…，Cn中必有一为假，因而S1必为不可满足的。
设S1是不可满足的，则对于不满足S1的任一解释I，可能有两种情况：
①I使C为真，则C1，C2，…，Cn中必有一子句为假，因而S是不可满足的。

注意这里假定C是由C1、C2归结得到的。

②I使C为假，则根据定理有C1∧C2为假，即I或使C1为假，或使C2为假，因而S也是不可满足的。
由此可见S和S1的不可满足性是等价的。[证毕]
　　同理可证Si和Si+1（由Si导出的扩大的子句集）的不可满足性也是等价的，其中i＝1，2，…。归结原理就是从子句集S出发，应用归结推理规则导出子句集S1，再从S1出发导出S2，依此类推，直到某一个子句集Sn出现空子句为止。根据不可满足性等价原理，已知若Sn为不可满足的，则可逆向依次推得S必为不可满足的。由此可以看出，用归结法证明定理，过程比较单纯，只涉及归结推理规则的应用问题，因而便于实现机器证明。