归结原理是1965年美国人Robinson提出的一种证明一阶谓词演算中定理的方法。使用这种方法时，对任一要证明的永真公式取非后，证明它不可满足，为此先转化成一种标准型，然后对这个标准型不断使用单一的推理规则，即实行归结，直到导出矛盾。

由谓词公式转化子句集的过程可以了解到：子句集中的子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。另外，空子句是不可满足的。因此，若一个子句集中包含空子句，则这个子句集一定是不可满足的。Robinson归结原理就是基于这一认识提出来的。其基本思想是：检查子句集S中是否包含空子句，若包含，则S不可满足；若不包含，就在子句集中选择合适的子句进行归结，一旦通过归结能推出空子句，就说明子句集S是不可满足的。

命题逻辑中的归结原理

若P是原子谓词公式，则称P与¬P为互补文字。

设C1与C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，那么从C1和C2中分别消去L1和L2，并将两个子句中余下的部分析取，构成一个新子句C12，则称这一过程为归结，称C12为C1和C2的归结式，称C1和C1为C12的亲本子句。

归结式C12是其亲本子句C1与C2的逻辑结论。

这个定理是归结原理中的一个很重要的定理，由它可得到如下两个推论：

设C1与C2是子句集S中的两个子句，C12是它们的归结式，若用C12代替C1和C2后得到新子句集S1，则由S1的不可满足性可推出原子句集S的不可满足性，即：S1的不可满足性⇒S的不可满足性

设C1与C2是子句集S中的两个子句，C12是它们的归结式，若把C12加入S中，得到新子句集S2，则S与S2在不可满足的意义上是等价的，即：S2的不可满足性<=>S的不可满足性

这两个推论给出了用归结原理证明子句集不可满足性的基本思想：为了要证明子句集S的不可满足性，只要对其中可进行归结的子句进行归结，并把归结式加入子句集S，或者用归结式替换它的亲本子句，然后对新子句集（S1或S2）证明不可满足性就可以了。如果经过归结能得到空子句，根据空子句的不可满足性，可得出原子句集S是不可满足的。

在命题逻辑中，对不可满足的子句集S，归结原理是完备的，即：若子句集不可满足，则必然存在一个从S到空子句的归结演绎；若存在一个从S到空子句的归结演绎，则S一定是不可满足的。但是，对于可满足的子句集S，用归结原理得不到任何结果。

归结原理

在谓词逻辑中，由于子句中含有变元，所以不可直接消去互补文字，而需要先用最一般合一对变元进行代换，然后才能进行归结。例如，设如下两个子句：

C1=P(x)∨Q(x)

C2=¬P(A)∨R(y)

由于P(x)与P(A)不同，所以C1与C2不能直接进行归结，但若用最一般合一

σ={A/x}

对两个子句分别进行代换：

C1σ=P(A)∨Q(A)，　C2σ=¬P(A)∨R(y)

就可对它们进行归结，消去P(A)与¬P(A)，得到如下归结式：

Q(A)∨R(y)

下面给出谓词逻辑中关于归结的定义。

定义1：设C1与C2是两个没有相同变元的子句，L1和L2分别是C1和C2中的文字，若σ是L1和¬L2的最一般合一，则称

C12=（C1σ－{L1σ}）∪（C2σ－{L2σ}）

为C1和C2的二元归结式，L1和L2称为归结式的文字。

一般来说，若子句C中有两个或两个以上的文字具有最一般合一σ，则称为Cσ为子句C的因子。如果Cσ是一个单文字，则称它为C的单元因子。

应用因子的概念，可对谓词逻辑中的归结原理给出如下定义。

定义2：子句C1和C2的归结式是下列二元归结式之一：

①C1与C2的二元归结式；

②C1与C2的因子C2σ2的二元归结式；

③C1的因子C1σ1与C2的二元归结式；

④C1的因子C1σ1与C2的因子C2σ2的二元归结式。

对于谓词逻辑，定理1仍然适用，即归结式是它的亲本子句的逻辑结论。用归结式取代它在子句集S中的亲本子句所得到的新子句仍然保持着原子句集S的不可满足性。

另外，对于一阶谓词逻辑，从不可满足的意义上说，归结原理也是完备的，即：若子句集是不可满足的，则必存在一个从该子句集到空子句的归结演绎；若从子句集存在一个到空子句的演绎，则该子句集是不可满足的。