3.3 归结推理方法

归结原理由杰森·鲁滨逊（J. A. Robinson）于 1965 年提出，又称为消解原理。该原理是鲁滨逊在Herbrand理论的基础上提出的一种基于逻辑、采用反证法的推理方法，由于其理论上的完备性，归结原理成为机器定理证明的主要方法。海伯伦（Herbrand）采用了反证法的思想，将永真性的证明问题转化为不可满足性的证明问题。Herbrand理论为自动定理证明奠定了理论基础，而鲁滨逊的归结原理使自动定理证明得以实现。

3.3.1 谓词公式化为子句集的方法

1）范式

（1）前束形范式

一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域一直延伸到公式之末，同时公式中不出现连接词“→”及“↔”，这种形式的公式称为前束形范式。例如，公式

即一个前束形的范式。

（2）斯克林范式

从前束形范式中消去全部存在量词所得到的公式，即斯克林（Skolem）范式，或称Skolem标准型。例如，如果用f（x）代替前束形范式中的y，即得Skolem范式：

Skolem标准型的一般形式是

其中，M（x ₁ ，x ₂ ，…，x _n ）是一个合取范式，称为Skolem标准型的母式。

将谓词公式化为Skolem标准型的步骤如下：

①消去谓词公式中的蕴涵（→）和双条件符号（↔），以¬A∨B ~A∨B代替A→B，以（A∧B）∨（¬A∧¬B）（A∧B）∨（¬A∧¬B）替换A↔B。

②减少否定符号（~）的辖域，使否定符号“~”最多只作用在一个谓词上。

③重新命名变元，使所有的变元的名字均不同，并且自由变元及约束变元也不同。

④消去存在量词。这里分两种情况：一种情况是存在量词不出现在全称量词的辖域内，此时，只要用一个新的个体常量替换该存在量词约束的变元就可以消去存在量词；另一种情况是存在量词位于一个或多个全称量词的辖域内，这时需要用一个Skolem函数替换存在量词来将其消去。

⑤把全称量词全部移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。

⑥母式化为合取范式，任何母式都可以写成由一些谓词公式和谓词公式否定的析取的有限集组成的合取。

需要注意的是，由于在化解过程中，消去存在量词时作了一些替换，一般情况下谓词公式的Skolem标准型与谓词公式本身并不等值。

例 3.2 将下式化为 Skolem 标准型 ：

解 第一步 ， 消去蕴涵符号 ， 得

第二步 ，¬ 深入量词内部 ， 得

第三步，变元易名，得

第四步，存在量词左移，直至所有的量词移到前面，得

由此得到前束形范式 ， 第五步 ， 消去存在量词 ， 略去任意量词 ， 消去 （∃y）， 因为它左边只 有 （∀x）， 所以使用 x 的函数 f（x） 代替 ， 消去 （∃u）， 同理使用 g（x） 代替 ， 这样可得

略去全程变量 ， 原式的 Skolem 标准型为 ：

2）子句与子句集

在谓词逻辑中，有下述定义：

①不含有任何连接词的谓词公式称为原子谓词公式，简称原子（atom），而原子谓词公式及其否定统称为文字（literal）。P称为正文字，¬P称为负文字。P与¬P为互补文字。

②子句（clause）就是由一些文字组成的析取式，任何文字本身也都是子句。

③不包含任何文字的子句称为空子句，记为NIL。因为空子句中不包含任何文字，不能被任何解释满足，所以空子句是永假的，不可满足的。

④由子句构成的集合称为子句集。

在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理归化成相应的子句集，从而能够比较容易地判定谓词公式的不可满足性。将谓词公式化为相应的子句集的过程与化为Skolem标准型的过程类似，但后续步骤较多，下面结合一个具体的例子，说明把谓词公式化成子句集的步骤。

例 3.3 将下列谓词公式化为子句集

解 第一步 ， 消去谓词公式中的蕴涵符号 ， 得

第二步，把否定符号内移，利用谓词公式的等价关系

双重否定律：

德摩根律：

量词转换律：

可得

第三步，变量标准化，使不同量词约束的变元有不同的名字，得

第四步，所有量词前移，且保证移动时不改变相对顺序，得

第五步，消去存在量词，使用x，y的函数代替，得

第六步，把母式化为合取范式，得

第七步，隐略去前束式，得

第八步，把母式用子句集表示，得

第九步，变量分离标准化，最终得到子句集

3）不可满足意义上的一致性

设有谓词公式G，其对应的子句集为S，则G是不可满足的充分必要条件为S是不可满足的。需要再次强调：公式G与其子句集S并不等值，知识在不同可满足意义下等价。

4）P =P ₁ ∧P ₂ ∧…P _n 的子句集

当P =P ₁ ∧P ₂ ∧…P _n 时，若设P的子句集为S _p ，P _i 的子句集为S _i ，则一般情况下，S _p 并不等于S ₁ ∪S ₂ ∪S ₃ ∪…∪S _n ，而是要比S ₁ ∪S ₂ ∪S ₃ ∪…∪S _n 复杂得多。但是，在不可满足的意义下，子句集S _p 与S ₁ ∪S ₂ ∪S ₃ ∪…∪S _n 是一致的，即

3.3.2 海伯伦（Herbrand）定理

Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理证明的。同时归结原理是Herbrand定理的具体实现，利用Herbrand定理对公式的证明是通过归结法进行的。

要判定一个子句集是不可满足的，则需要判定该子句集中的每一个子句都是不可满足的；要判定一个子句是不可满足的，则需要判定该子句对任何非空个体域的任意解释都是不可满足的。可见，判定子句集的不可满足性是一项非常困难的工作。最重要的问题是一阶逻辑公式的永真性或永假性的判定是否能在有限步内完成。

Herbrand定理思想如下：

要证明一个公式是永假的，采用反证法的思想（归结原理），就是要寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，那么就没有这样的解释存在，并且算法在有限步内停止。因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无限的、不可数的，要找到所有解释是不可能的。Herbrand定理的思想是简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上（此域称为H域），原子谓词公式仍然是不可满足的，即保证不可满足的性质不变。H域和D域的关系如图 3.5 所示。

1）H域

定义 3.1 设S为子句集合，S的H域H（S）可定义如下：

（1）S中的一切常量字母均出现在H（S）中，若S中无任何常量字母，则命名一个常量字母a，使a∈H（S）。

（2）若项t ₁ ，…，t _n ∈H（S），则f ⁿ （t ₁ ，…，t _n ）∈H（S），其中，f为S中的任意函数。

（3）H（S）中的项仅由（1）和（2）形成。

为了讨论子句集S在H域上的真值，引入H域上S的原子集A，它是S中谓词公式的实例集。

定义 3.2 设S是子句集，对应的H域上的原子集A为所有出现在S中的原子谓词公式实例。

（1）如果原子谓词公式为命题（不包含变量），则其实例就是其本身。

（2）若原子公式形如P（t ₁ ，…，t _n ），t _i 为变量（i = 1，2，…，n），则其实例就是用S的H域中的元素代替t ₁ ，…，t _n 形成的。

例 3.4 设子句集 S 丨= {P（a），Q（x）∨R（f（x））}， 求 H 域 。

解 在此题中只有一个常量 a

2）H解释

解释 I 谓词公式G在论域D上任何一组真值的指定称为一个解释。公式G的一个解释就是公式G在其论域上的一个实例化。

H 解释 子句集S在其H域上的解释称为H解释。

I是H域下的一个指派。简单地说，原子集A中的各元素真假组合都是H的解释（或真或假只取一个），或者说凡是对A中各元素真假值的一个具体设定或对S中出现的常量、函数及谓词的一次取值就构成S的一个H解释。

为谓词公式建立子句集S，又建立H域、原子集A，目的是希望定义在一般论域D上，使S为真的任一解释I，可由S的H域上的某个解释I ^∗ 实现。这样，才能真正做到任意论域D上S为真的问题，转化成仅有可数个元素的H域上S为真的问题。从而子句集S在D上满足问题转化成了H上的不可满足的问题。

如下的 3 个定理保证了归结法的正确性：

定理 3.1 设I是S的论域D上的解释，存在对应于I的H解释I ^∗ ，使得若有S 丨 _I = T，必有S 丨 _I∗ = T。

定理 3.2 子句集S是不可满足的，当且仅当S的一切H解释都为假。

定理 3.3 子句集S是不可满足的，当且仅当每一个解释I下，至少有S的某个子句的某个基例为假。

3）语义树

由H解释的定义可以看出，通常子句集合S的H解释的个数是可数的，这样可以使用“语义树”枚举出S的所有可能的H解释，形象地描述子句集在H域上的所有解释，以观察每个分支对应的S的逻辑真值是真还是假。当子句集包含的原子公式均为命题时，其原子集是有限集，很容易画出完整的语义树。

例 3.5 令 A = {P，Q，R} 是子句集合 S 的原子集合 ， 画出其语义树 。

解 由于每个基原子只可能有两个真值 （T 和 F）， 因此很容易以二叉树的形式建立语义 树 ， 图 3.6 所示为 S 的完整语义树 。

从图 3.6 中可以看出 ， 从树根节点 n ₀ 到叶节点 n 的路径就指示了一个解释 ， 记为 I（n）， 其表示为路径上标记的集合 ， 每个标记是一个文字 。 如 I（n ₃₁ ）= 丨P，Q，R}。丨 可以对语义树指 示的每个解释，判别子句集的真假性，进而判别子句集是永真、可满足还是不可满足的。

对一般的子句集，H是可数无穷集，从而相应的语义树也可能成为一棵无穷树。对无穷语义树，如果子句集是不可满足的，则不必无限地扩展语义树就可以确定语义树上的所有路径都分别对应一个导致子句集不可满足的解释，这样的语义树称为封闭语义树。

4）Herbrand定理

在上述研究工作的基础上，海伯伦提出了Herbrand定理，该定理是符号逻辑中的重要定理，是机器定理证明的基础。由H解释的性质可知，若子句集S按它的任一H解释都为假，则可以断定S是不可满足的。通常S的H解释的个数是可数个，可以使用语义树组织它们。

定理 3.4（Ⅰ型Herbrand定理）子句集S是不可满足的，当且仅当相应S的每个完全语义树都存在有限封闭的语义树。

证明 设S是不可满足的，令T为S的任一完全语义树。

对T中由根节点出发的到达任一叶节点的路径B，令I _B 为对应B分支上S的一个解释。因为S是不可满足的，I _B 必使得S中某子句C的一个基例C′为假。然而，由于C′是有限的，因此路径B上必存在一个失败节点N _B 。

因为T的每条这样的路径上都有一个失败节点，所以S存在封闭的语义树T′。反之，若相应S的每个完全语义树都存在一棵有限封闭语义树，则其中由根节点出发的每条路径都含有失败节点。因为S的任一解释都对应T的某一分支，这说明每个解释都使得S的某个子句的基例为假。所以S是不可满足的。证毕。

定理 3.5（Ⅱ型Herbrand定理）子句集合S是不可满足的，当且仅当存在不可满足的S的有限基例集S′。

Ⅱ型Herbrand定理提出了一种反驳程序，即给定一个预证明的不可满足的子句集合S，若存在机械程序能逐次产生S中子句的基例的集合 ，…，并且能逐次检验 ，…的不可满足性，则由Herbrand定理可知，能找出一个有限的n，使 是不可满足的。

这种方法效率比较低，因为即使对只有 10 个两文字基子句的情况也有 2 ¹⁰ 个合取式，所以化成析取范式并不是好的方法，故可以采用下列规则简化计算过程。

（1）重言式规则

设从子句集合SS中删除所有重言式得出子句集合S′S′，则S′S′是不可满足的，当且仅当SS是不可满足的。

（2）单文字规则

如果在子句集SS中存在只有一个文字的基子句L，删除SS中包含L的所有基子句得S′S′，则：

①若S′S′是空的，则SS是可满足的；

②若S′S′非空，在S′S′中删除所有文字¬L得S″S″，则SS不可满足，当且仅当S″S″不可满足。

（3）纯文字规则

当文字L出现在SS中，而¬L不出现在SS中时，则说L为SS的纯文字。

如果SS中的文字L是纯的，删除SS中所有包含L的基子句得S′S′，则：

①若S′S′是空集，则SS可满足；

②若S′S′非空，则SS不可满足，当且仅当S′S′不可满足。

（4）分裂规则

若子句集SS可以写成如下形式：

其中，A _i 、B _i 、R与L和¬L无关，则求出集合

S是不可满足的，当且仅当S ₁ 和S ₂ 都是不可满足的。运用Herbrand定理并借助语义树方法，从理论上讲可以建立计算机程序实现自动定理证明，但在实际中是很难行得通的。

定理 3.6（归结原理的完备性）子句集合S是不可满足的，当且仅当存在使用归结推理规则由S对空子句的演绎。

需要注意以下几点：

①归结原理是半可判定的，即如果S不是不可满足的，则使用归结原理方法可能得不到任何结果。

②归结原理是建立在Herbrand定理之上的。

③在子句集S中允许出现等号或不等号时，归结法就不完备了。

④归结方法是一种可以机械化实现的方法，它是Prolog语言的基础。

3.3.3 鲁滨逊（Robinson）归结原理

鲁滨逊归结原理又称为消解原理，是鲁滨逊提出的一种证明子句集不可满足性，实现定理证明的一种理论及方法。它是机器定理证明的基础。

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

下面对命题逻辑及谓词逻辑分别给出归结的定义。

1）命题逻辑中的归结原理

定义 3.3 设C ₁ 与C ₂ 是子句集中的任意两个子句，如果C ₁ 中的文字L ₁ 与C ₂ 中的文字L ₂ 互补，那么从C ₁ 和C ₂ 中分别消去L ₁ 和L ₂ ，并将两个子句中余下的部分析取，构成一个新子句C ₁₂ ，这一过程称为归结。C ₁₂ 称为C ₁ 和C ₂ 的归结式，C ₁ 和C ₂ 称为C ₁₂ 的亲本子句。

下面举例说明具体的归结方法。

例如，在子句集中取两个子句C ₁ = P，C ₂ = ¬P，可见，C ₁ 和C ₂ 是互补文字，则通过归结可得归结式C ₁₂ =NIL。这里的NIL代表空子句。

又如，设C ₁ = ¬P∨Q∨R，C ₂ = ¬Q∨S，可见，这里的L ₁ = Q，L ₂ = ¬Q，通过归结可得归结式C ₁₂ = ¬P∨R∨S。

例如，设C ₁ = ¬P∨Q，C ₂ = ¬Q∨R，C ₃ = P。首先对C ₁ 和C ₂ 进行归结，得到C ₁₂ = ¬P∨R，然后再用C ₁₂ 与C ₃ 进行归结，得到C ₁₂₃ =R。同样的例子，如果先对C ₁ 与C ₃ 进行归结，然后再把其归结式与C ₂ 进行归结，将得到相同的结果。归结过程也可用一棵树直观地表示出来，上述归结过程可用图 3.7 表示。

定理 3.7 归结式C ₁₂ 是其亲本子句C ₁ 和C ₂ 的逻辑结论。即如果C ₁ 和C ₂ 为真，则C ₁₂ 为真。

证明 设 通过归结可得 和 的归结式

因为

所以

根据假言三段论得

又因为

所以

由逻辑结论的定义知，即由C ₁ ∧C ₂ 的不可满足性可推出C ₁₂ 的不可满足性，可知C ₁₂ 是其亲本子句C ₁ 和C ₂ 的逻辑结论。证毕。

这个定理在归结原理中非常重要，由它可以得到如下两个重要的推论。

推论 1 设C ₁ 与C ₂ 是子句集S中的两个子句，C ₁₂ 是它们的归结式，若用C ₁₂ 代替C ₁ 与C ₂ 后得到新子句集S ₁ ，则由S ₁ 不可满足性可推出原子句集S的不可满足性，即

S ₁ 的不可满足性⇒S的不可满足性

推论 2 设C ₁ 与C ₂ 是子句集S中的两个子句，C ₁₂ 是它们的归结式，若把C ₁₂ 加入原子句集S中，得到新子句集S ₂ ，则S与S ₂ 在不可满足的意义上是等价的，即

S ₂ 的不可满足性⇔S的不可满足性

这两个推论说明：为了证明子句集S的不可满足性，只要对其中可进行归结的子句进行归结，并把归结式加入子句集S，或者用归结式替换它的亲本子句，然后对新子句集（S ₁ 或S ₂ ）证明不可满足性即可。注意到空子句是不可满足的，因此，如果经过归结能得到空子句，则立即可得原子句集S是不可满足的结论。这就是用归结原理证明子句集不可满足性的基本思想。

2）谓词逻辑中的归结原理

在谓词逻辑中，由于子句中含有变元，因此不像命题逻辑那样可直接消去互补文字，而需先用最一般合一对变元进行代换，然后才能进行归结。

例如，设有下列两个子句

由于P（x）与P（a）不同，因此C ₁ 与C ₂ 不能直接进行归结，但若用最一般合一

对两个子句分别进行代换

就可以对它们进行直接归结，消去P（a）与¬P（a），得到如下归结式

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

定义 3.4 设C ₁ 与C ₂ 是两个没有相同变元的子句，L ₁ 和L ₂ 分别是C ₁ 和C ₂ 的文字，若σ是L ₁ 和¬L ₂ 的最一般合一，则称

为C ₁ 和C ₂ 的二元归结式。

例 3.6 设 C ₁ =P（x）∨Q（a），C ₂ = ¬P（b）∨R（x）， 求其二元归结式 。

解 由于 C ₁ 与 C ₂ 有相同的变元 ， 不符合定义要求 ， 因此需要修改 C ₂ 中变元 x 的符号 ， 令 C ₂ = ¬P（b）∨R（y）。 此时 L ₁ =P（x），L ₂ = ¬P（b）。

L ₁ 和 ¬L ₂ 的最一般合一 σ= {b / x}， 则

如果在参加归结的子句内部含有可合一的文字，则在归结之前应对这些文字先进行合一。

定义 3.5 子句C ₁ 和C ₂ 的归结式是下列二元归结式之一：

（1）C ₁ 与C ₂ 的二元归结式；

（2）C ₁ 的因子C ₁ σ ₁ 与C ₂ 的二元归结式；

（3）C ₁ 与C ₂ 的因子C ₂ σ ₂ 的二元归结式；

（4）C ₁ 的因子C ₁ σ ₁ 与C ₂ 的因子C ₂ σ ₂ 的二元归结式。

与命题逻辑中的归结原理相同，对谓词逻辑，归结式是其亲本子句的逻辑结论。用归结式取代它在子句集S中的亲本子句所得到的新子句集仍然保持原子句集S的不可满足性。

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

需要指出的是，如果没有归结出空子句，则既不能说S不可满足，也不能说S是可满足的。因为可能S是可满足的，而归结不出空子句，也可能是因为还没有找到合适的归结演绎步骤，而归结不出空子句。

3.3.4 归结反演

归结原理给出了证明子句集不可满足性的方法。应用归结原理证明定理的过程称为归结反演。设F为已知前提的公式集，Q为目标公式（结论），用归结反演证明Q为真的步骤如下：

①写出谓词关系公式；

②用反演法写出谓词表达式；

③化为Skolem标准型；

④求取子句集S;

⑤对S中可归结的子句做归结；

⑥归结式仍放入S中，反复归结过程；

⑦得到空子句；

⑧命题得证。

例 3.7 已知下列事实 ： 任何通过历史考试并中了彩票的人是快乐的 ； 任何肯学习或幸运 的人可以通过所有考试 ;John 不学习但很幸运 ； 任何人只要幸运就能中彩 。 求证 :John 是快 乐的 。

结论得证。

3.3.5 利用归结原理求解问题

归结原理除可用于定理证明外，还可用来求取问题的答案，其思想与定理证明类似。下面给出应用归结原理求解问题的步骤：

①已知前提用谓词公式表示出来，并且化为相应的子句集，设该子句集的名字为S。

②待求解的问题也用谓词公式表示出来，然后将其否定并与答案谓词ANSWER构成析取式，ANSWER是一个为了求解问题而专设的谓词，其变元必须与问题公式的变元完全一致。

③将第二步中得到的析取式化为子句集，并将该子句集并入子句集S中，得到子句集S′。

④对S′应用归结原理进行归结，并把每次归结得到的归结式都并入S′中。如此反复进行，若得到归结式ANSWER，则答案就在ANSWER中。

例 3.8 设 Tony、Mike 和 John 属于 A 俱乐部 ，A 俱乐部的成员不是滑雪运动员就是登山 运动员 。 登山运动员不喜欢雨 ， 而且任何不喜欢雪的人都不是滑雪运动员 。Mike 讨厌 Tony 所喜欢的一切东西 ， 而喜欢 Tony 所讨厌的一切东西 。Tony 喜欢雨和雪 。 试用谓词公式的集 合表示这段知识 ， 用归结原理回答问题 ：“ 谁是 A 俱乐部的一名成员 ？ 他是一名登山运动员但 不是滑雪运动员 ？”

解 （1） 定义谓词

A（x）:x 是 A 的一个成员 ；

B（x）:x 是滑雪运动员 ；

C（x）:x 是登山运动员 ；

L（x，y）:x 喜欢 y。

（2） 将前提表示成谓词公式

A（Tony）；

A（Mike）；

A（John）；

（∀x）（A（x）→[B（x）∧¬C（x）]∨[¬B（x）∧C（x）]）；

（∀x）（C（x）→¬L（x，Rain））；

（∀x）（¬L（x，Snow）→¬（B（x））；

（∀x）（L（Tony，x）→¬L（Mike，x））；

（∀x）（¬L（Tony，x）→L（Mike，x））；

L（Tony，Rain）；

L（Tony，Snow）。

（3） 将前提化为子句集

①A（Tony）；

②A（Mike）；

③A（John）；

④¬A（x）∨B（x）∨¬B（x）；

⑤¬A（x）∨B（x）∨C（x）；

⑥¬A（x）∨¬B（x）∨¬C（x）；

⑦¬A（x）∨¬C（x）∨C（x）；

⑧¬C（x）∨¬L（x，Rain）；

⑨L（x，Rain）∨¬B（x）；

⑩¬L（Tony，x）∨¬L（Mike，x）；

⑪L（Tony，x）∨L（Mike，x）；

⑫L（Tony，Rain）；

⑬L（Tony，Snow）。

（4） 将待求解的问题表示成谓词公式 ， 然后否定 ， 并与答案谓词析取

化为子句集：

⑭¬A（x）∨¬C（x）∨B（x）∨ANSWER（x）。

（5） 归结过程

因此 ，Mike 是 A 俱乐部的一名成员 ， 他是一名登山运动员 ， 但不是滑雪运动员 。 KEqZMLP20Lp2cXDKXgdLcg36SA2i/j3+R74SeILgLqliy3TNT1IpdmmqCSIH/j8N