3.4 归结演绎推理

人工智能的目的之一就是使计算机能模拟人的智能，自动定理证明不仅能使许多数学问题经过定理证明得到解决，而且可以使许多非数学问题（如机器人、专家系统）等得到解决。从自然演绎推理我们已经看到，即使是非常简单的结论证明也需要许多步骤才能完成，而且在证明的过程中，需要牵涉匹配、代换、假言推理等步骤。我们很自然地就会想到是否能让计算机来完成定理的证明。但是构造实际程序让机器生成自动证明并不是件容易的事情。海明伦和鲁滨逊在自动定理证明方面取得了卓越的成绩，提出了相应的理论和方法。海明伦提出的海明伦域和海明伦定理为自动定理的证明奠定了理论基础。鲁滨逊原理使定理证明的机械化变为现实。

若欲证明前提条件P可推导出结论Q，即证明P→Q永真，由真值表3.1可以得到该问题的证明等价于证明P∧￢Q永假，即P∧￢Q是不可满足的。

表3.1 P→Q的真值表

在本节中，首先讨论子句和子句集的概念，然后介绍海明伦理论和鲁滨逊归结原理，最后讲述归结策略以及如何用归结原理证明和求解问题的方法。

3.4.1 子句

定义3.14 不含有任何连接词的谓词公式称为原子谓词公式。

定义3.15 原子谓词公式及其否定统称为文字。

例3.5 P（x），Q（x，y）都为文字。

定义3.16 任何文字的析取式称为子句。

例3.6 P（x）∨￢Q（x，y），P（x）∨R（y）都为子句。

定义3.17 不包含任何文字的子句为空子句。

由于空子句不含有任何文字，它不能被任何解释满足，所以空子句是永假式，是不可满足的。

定义3.18 由子句构成的集合称为子句集。

在谓词演算中，任何谓词公式都可化成相应的子句集。对于给定的谓词公式G，首先化成与其等价的前束范式：

（Q1x1）…（Qnxn）M（x1，…，xn）

其中，Qi（i=1，2，…，n）是存在量词或全称量词。在式M（x1，…，xn）中不再含有量词。

然后将M（x1，…，xn）化成等价的合取范式。

最后将存在量词消去，得到公式G的Skolem标准形，进而得到公式所相应的子句集。

下面给出谓词公式化成子句集的步骤。

（1）消去“→”和“↔”。利用下列等价关系消去谓词公式中的“→”和“↔”。

P→Q⇔￢P∨Q，P↔Q⇔（P∧Q）∨（￢P∧￢Q）

（2）“￢”仅靠谓词。利用下列等价关系把“￢”移到紧靠谓词的位置上。

￢（￢P）⇔P，￢（P∧Q）⇔￢P∨￢Q，￢（P∨Q）⇔￢P∧￢Q，￢（∃x）P⇔（∀x）￢P

（3）相同约束变元换名。若有相同名字的约束变元，则需对相同名字变元进行换名。

（4）消去存在量词。

若存在量词不出现在全称量词的辖域内，则用一个新的个体常量去取代。

若存在量词出现在全称量词的辖域内，则用全称量词的函数去取代存在量词。

例如，对（∃y）（∀x1）（∀x2）…（∀xn）P（x1，x2，…，xn，y），由于存在量词y不被全称量词约束，所以y可用一个新的个体常量如a取代。消去存在量词后可以得到：

（∀x1）（∀x2）…（∀xn）P（x1，x2，…，xn，a）

例如，（∀x1）（∀x2）…（∀xn）（∃y）P（x1，x2，…，xn，y），由于在此式中存在量词y被全称量词x1，x2，…，xn约束，所以将存在量词y表示成全称量词的函数f（x1，x2，…xn），消去存在量词后得到：

（∀x1）（∀x2）…（∀xn）P（x1，x2，…，xn，f（x1，x2，…，xn））

（5）将全称量词移到公式的左边。

（6）利用等价关系P∨（Q∧R）⇔（P∨Q）∧（P∨R），将公式化为合取范式。

（7）消去全称量词。

（8）使不同子句中的变元不同名。

（9）消去合取词，生成子句集。

例3.7 将公式（∃z）（∀x）（（∀y）P（x，y）→￢（∀y）（Q（x，y）→R（z，y）））化为子句集。

（1）消去“→”和“↔”。

（∃z）（∀x）（￢（∀y）P（x，y）∨￢（∀y）（￢Q（x，y）∨R（z，y）））

（2）“￢”紧靠谓词。

（∃z）（∀x）（（∃y）￢P（x，y）∨（∃y）（Q（x，y）∧￢R（z，y）））

（3）相同约束变元换名。

（∃z）（∀x）（（∃y）￢P（x，y）∨（∃u）（Q（x，u）∧￢R（z，u）））

（4）消去存在量词。

（∀x）（￢P（x，f（x））∨（Q（x，g（x））∧￢R（a，g（x））））

（5）将公式化为合取范式。

（∀x）（（￢P（x，f（x））∨Q（x，g（x）））∧（￢P（x，f（x））∨￢R（a，g（x））））

（6）消去全称量词。

（￢P（x，f（x））∨Q（x，g（x）））∧（￢P（x，f（x））∨￢R（a，g（x）））

（7）使不同子句中的变元不同名。

（￢P（x，f（x））∨Q（x，g（x）））∧（￢P（y，f（y））∨￢R（a，g（y）））

（8）消去合取词，生成子句集。

{￢P（x，f（x））∨Q（x，g（x）），￢P（y，f（y））∨￢R（a，g（y））}

3.4.2 Herbrand理论

对于谓词公式来说，若需证明其不可满足性，需对个体域的所有个体进行考察，只有当个体域上的任何解释都是不可满足时，谓词公式才是不可满足的。由于个体域的任意性以及解释个数的无限性，所以不可满足的证明是困难的。海明伦构造了一个特殊的域，并证明只要对这个域上的一切解释进行判定，就可得知子句集是否不可满足，这个域称为海明伦域，即H域。

1.H域

定义3.19 设S是子句集，定义在个体域D上，按以下步骤可得到S的H域（H∞）。

（1）令H0是S中所出现的常量集合。若S中没有常量出现，就任取常量a∈D，规定H0={a}。

（2）Hi=Hi-1∪{所有形如f（t1，…，tn）的元素}，其中f（t1，…，tn）是出现于S中的任一函数符号，而t1，…，tn是Hi-1的元素，i=1，2，…。

例3.8 求子句集S={P（x），Q（f（x））∨￢R（x）}的H域。

解：H0={a}

H1=H0∪{f（a）}={a，f（a）}

．

．

．

H2=H1∪{f（a），f（f（a））}={a，f（a），f（f（a））}

H∞={a，f（a），f（f（a）），…}

例3.9 求子句集S={￢P（x），P（y）∨Q（y）}的H域。

解：H0={a}

H1=H0H2=H1

.

.

.

H∞={a}

例3.10 求子句集S={P（f（x））∨Q（a），Q（g（y））∨R（b）}的H域。解：H0={a，b}

H1=H0∪{f（a），f（b），g（a），g（b）}={a，b，f（a），f（b），g（a），g（b）}

H2={a，b，f（a），f（b），g（a），g（b），f（f（a）），f（f（b）），f（g（a）），f（g（b）），g（f（a）），

g（f（b）），g（g（a）），g（g（b））}

H∞=H0∪H1∪H2∪…

2.原子集

定义3.20 令集合A={所有形如P（t1，…，tn）的元素}，称做子句集S的原子集，其中P（t1，…，tn）是出现在S中的任一谓词符号，t1，…，tn是S的H域的任意元素。

例3.11 求例3.8的原子域。

解：在例3.8中已求得H∞={a，f（a），f（f（a）），…}，则原子域

A={P（a），Q（a），R（a），P（f（a）），Q（f（a）），R（f（a）），P（f（f（a））），Q（f（f（a））），R（f（f（a）））}

例3.12 求例3.9的原子域。

解：在例3.9中已求得H∞={a}，则原子域A={P（a），Q（a）}。

定义3.21 将没有变元出现的原子、文字、子句和子句集分别称做基原子、基文字、基子句和基子句集。

定义3.22 当子句集S中的某个子句C中的所有变元符号均以其H域中的元素替换时，所得到的基子句称做C的一个基例。

例3.13 对于子句集S={P（a），￢P（x）∨P（f（x））}，有H∞={a，f（a），f（f（a）），…}，子句P（a）是基子句，而且a∈H，所以P（a）又是基例。对于子句￢P（x）∨P（f（x）），取b∈D得到基子句￢P（b）∨P（f（b）），但￢P（b）∨P（f（b））不是基例。取f（a）∈H，则￢P（f（a））∨P（f（f（a）））为基例。

3.H解释

由子句集S建立H域、原子集A，希望定义于一般个体域D上使S为真的任一解释I，可由S的H域上的某个解释I﹡来实现。这样，便使任一个体域D上S为真的问题转换成了仅有可数个元素的H域上S为真的问题了。从而子句集S在D上的不可满足问题转化成了H域上的不可满足问题。

例3.14 设子句集S={P（x）∨Q（x），R（f（y））}，构造在个体域D上的一个解释I，并由此构造H域上的解释I﹡。

解：H∞={a，f（a），f（f（a）），…}

原子域A={P（a），Q（a），R（a），P（f（a）），Q（f（a）），R（f（a）），…}

对个体域D={1，2}，做如下的解释I：

f（1）=2 f（2）=2 P（1）=T P（2）=F

Q（1）=F Q（2）=T R（1）=F R（2）=T

S={P（x）∨Q（x），R（f（y））}的逻辑含义为（∀x）（∀y）（（P（x）∨Q（x））∧R（f（y）））。

当x=1时，P（1）∨Q（1）=T

当x=2时，P（2）∨Q（2）=T

当y=1时，f（1）=2R（f（1））=T

当y=2时，f（2）=2R（f（2））=T

（∀x）（∀y）（（P（x）∨Q（x））∧R（f（y）））在解释I下为真。

D域上解释I所对应的H域上的解释I﹡如下。

若a=1，H域上的元素值：f（a）=f（1）=2，f（f（a））=f（2）=2，…，P（a）=P（1）=T，Q（a）=Q（1）=F，R（a）=R（1）=F，P（f（a））=P（2）=F，Q（f（a））=Q（2）=T，R（f（a））=R（2）=T。

可得到解释：

={P（a），￢Q（a），￢R（a），￢P（f（a）），Q（f（a）），R（f（a）），…}

当a=2时，H域上的元素值：f（a）=f（2）=2，f（f（a））=f（2）=2，…，P（a）=P（2）=F，Q（a）=Q（2）=T，R（a）=R（2）=T，P（f（a））=P（2）=F，Q（f（a））=Q（2）=T，R（f（a））=R（2）=T。

可得到解释：={￢P（a），Q（a），R（a），￢P（f（a）），Q（f（a）），R（f（a）），…}

可验证，S|=T，S|=T。

定理3.1 设I是子句集S的个体域D上的解释，存在对应于I的H解释I﹡，使得若有S|I=T，则必有S|I﹡=T。

定理3.2 子句集S是不可满足的，当且仅当所有的S在H解释下为假。

定理3.3 子句集不可满足的充要条件是存在一个有限的不可满足的基子句集S′。该定理称为Herbrand定理。

3.4.3 鲁滨逊归结原理

谓词公式F，其对应的子句集为S，公式F不可满足的充要条件是S不可满足。在子句集中，子句与子句之间的关系是合取的，若其中一个子句是不可满足的，则该子句集是不可满足的。我们已知空子句是不可满足的，若一个子句集包含空子句，则该子句集一定是不可满足的。

鲁滨逊归结原理的基本思想是：检查子句集S中是否能归结出或包含空子句，若能归结出或包含空子句，则S不可满足；否则S可满足。

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

定义3.23 若P是原子谓词公式，则称P和￢P为互补文字。

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

例3.15 设C1=P和C2=￢P，求其归结式C12。

解：C12=NIL

NIL表示空子句。

例3.16 设C1=￢P∨Q，C2=P∨Q，C3=￢Q∨R，求其归结式C123。

解：

由C1和C2得

C12=Q

由C12和C3得

C123=R

定理3.4 归结式C12是其亲本子句C1和C2的逻辑结论。下面对该定理进行证明。

证明：设C1=L∨C′1，C2=￢L∨C′2。

通过归结可得到：

C12=C′1∨C′2

C1=L∨C′1⇔￢C′1→L C2=￢L∨C′2⇔L→C′2

C1∧C2⇔（￢C′1→L）∧（L→C′2）⇒￢C′1→C′2⇔C′1∨C′2=C12

所以，C1∧C2⇒C12。

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

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

推论3.2 设C1与C2是子句集S中的两个子句，C12是它们的归结式，若C12加入S后得到新子句集S2，则由S2的不可满足性可推出原子句集S的不可满足性，即

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

以上的两个推论表明：在证明子句集S的不可满足性时，只要选择子句进行归结，并将归结式加入子句集S，或者用归结式取代亲本子句，即可得到新的子句集S′。若经过归结能够归结出空子句，则说明原子句集S不可满足。

例3.17 设有子句集S={￢P∨￢Q∨R，P∨R，Q∨R，￢R}，求证该子句集是不可满足的。

证明：

①￢P∨￢Q∨R

②P∨R

③Q∨R

④￢R

⑤￢Q∨R　　　①与②归结

⑥R　　　　　　③与⑤归结

⑦NIL　　　　　④与⑥归结

所以，该子句集是不可满足的。

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

在谓词逻辑中，由于子句中含有变元，所以需要对变元进行合一和置换，才能进行归结。

例如，有子句C1=P（x）∨Q（x）和C2=￢P（a）∨R（y），此时不能像命题逻辑那样直接消去互补文字，但是会发现其中有可能互补的文字是P（x）和￢P（a）。若用最一般合一为σ={a/x}，则经过σ代换后，P（x）和￢P（a）是互补的。

对C1和C2进行代换：

C1σ=P（a）∨Q（a）

C2σ=￢P（a）∨R（y）

对C1σ和C2σ进行归结，得到归结式Q（a）∨R（y）。

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

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

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

例3.18 C1=P（x）∨Q（x），C2=￢P（a）∨R（y），求其归结式C12。

解：L1=P（x），L2=￢P（a），则σ={a/x}是L1和￢L2的最一般合一。

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

=（{P（a），Q（a）}-{P（a）}）∪（{P（a），R（y）}-{P（a）}）

={Q（a），R（y）}

=Q（a）∨R（y）

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

（1）C1与C2的二元归结式。

（2）C1与C2的因子C2σ2的二元归结式。

（3）C1的因子C1σ1与C2的二元归结式。

（4）C1的因子C1σ1与C2的因子C2σ2的二元归结式。

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

在归结的过程中，特别需要注意以下问题：

（1）确保每个子句有不同的变元名，以免在归结的过程中产生不便或错误。

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

例如，有两个子句C1=P（x）∨P（f（a））∨Q（x）和C2=￢P（y）∨R（y），求其归结式C12。

由于C1中有可合一的文字P（x）和P（f（a）），它们的最一般合一为σ1={f（a）/x}，则

C1σ1=P（f（a））∨Q（f（a））

C1σ1中的文字L1=P（f（a））和C2中的文字L2=￢P（y）是经代换可互补的文字。L1和￢L2的最一般合一是σ2={f（a）/y}。所以

C2σ2=￢P（f（a））∨R（f（a））

因此归结式C12=Q（f（a））∨R（f（a））。

（3）在求归结式时，若两个子句中有两对可互补的文字，不能同时消去，否则会产生错误。

例如，设有两个子句C1=P∨￢Q和C2=￢P∨Q，在C1和C2中有两对互补的文字P和￢P及Q和￢Q。若同时消去，就会得到空子句NIL，由于空子句是一个不可满足的式子，所以会推导出子句集{C1，CC2}是不可满足的错误结论。实际上子句集{C1，C2}是可满足的。

例3.19 设有子句集：

{￢R（x，y）∨￢Q（y）∨P（f（x）），￢R（u，v）∨￢Q（v）∨W（u，f（u）），￢P（z），R（A，B），Q（B）}判断该子句集是否可满足。

解：

①￢R（x，y）∨￢Q（y）∨P（f（x））

②￢R（u，v）∨￢Q（v）∨W（u，f（u））

③￢P（z）

④R（A，B）

⑤Q（B）

⑥￢R（x，y）∨￢Q（y）①与③归结{f（x）/z}

⑦￢Q（B）　　　　　　　④与⑥归结{A/x，B/y}

⑧NIL　　　　　　　　　⑤与⑦归结

3.4.4 归结策略

在归结的过程中，面临着大子句集而引起的演绎效率问题，解决问题的关键是如何在子句集中选择可归结的子句对进行归结，选择哪些子句对进行归结能够加速归结的过程，尽快地归结出空子句。最普通的归结过程是对子句集中的子句逐对进行比较，对可归结的子句进行归结，得到新的归结式。进行完一轮归结和比较后，再进行下一轮，如此反复，直到归结出空子句。这种归结方法会产生许多无用的归结式，而且占用了许多存储空间，花费了时间，降低了求解的效率。为解决这一问题，人们开始研究归结策略，以便选取合适的策略尽快归结出空子句。归结策略可分为两大类：一类是删除策略，删除某些无用的子句来缩小归结的范围；另一类是对参加归结的子句进行限制，尽可能地减小归结的盲目性，使其尽快地归结出空子句。

首先引入归结策略完备性的概念。归结策略的完备性是指若子句集是不可满足的，则一定存在着一个从子句集到空子句的归结过程。

1.删除策略

参与归结的子句越多，时间空间的耗费也就越大。若在归结之前，将无用的子句删除，则可减小搜索范围，提高归结效率。删除策略正是基于这一思想提出的，主要有以下的删除策略。

（1）纯文字删除法

如果某文字L在子句集中不存在可与之互补的文字￢L，则称该文字为纯文字。显然，在归结时纯文字不能被删除，因而包含纯文字的子句不可能归结出空子句，所以包含纯文字的子句对归结是无意义的，可将它从子句集中删除。

例如，有子句集S={P∨Q∨R，￢Q，￢R∨Q}，其中P是纯文字，所以从S中删除子句P∨Q∨R。

（2）重言式删除法

若一个谓词公式的真值永为真，则该命题为重言式或永真式。任何谓词公式A与重言式相与，其真值与谓词公式A相同。子句集中子句之间的关系是合取关系，所以不管是增加或减少一个真值为真的子句，都不会影响它的不可满足性，因而从子句集中可删除重言式。

例如，P（x）∨￢P（x）、Q（x）∨￢Q（x）都是重言式，此类重言式都可从子句集中删除。

（3）包孕删除法

设有子句C1和C2，如果存在一个代换σ使得C1σ⊆C2，则称C1包孕于C2。

例如，C1=P（x），C2=P（a）∨Q（a），若取σ={a/x}，便有

C1σ=P（a）⊂{P（a），Q（a）}

则C1包孕于C2。

例如，C1=P（x）∨Q（y），C2=P（a）∨Q（u）∨R（w），若取σ={a/x，u/y}，便有

C1σ={P（a），Q（u）}⊂{P（a），Q（u），R（w）}

则C1包孕于C2。

把子句集中包孕的子句C2删除后，不会影响子句集的不可满足性，因而可从子句集中删除。

2.限制策略

（1）支持集策略

若要证明由前提条件F：A1∧A2∧…∧An能推导出结论G，则需证明A1∧A2∧…∧An∧￢G是不可满足的。分析矛盾出现的原因，极有可能是由于￢G的引入，导致了矛盾。很自然地就会想到如下限制：每次归结时，亲本子句中至少有一个子句来自于结论的否定式￢G，或其导出的归结式。该策略就是支持集策略，此策略是完备的。

例3.20 设有子句集S={P∨Q，￢P∨R，￢Q∨R，￢R}，其中￢R是目标公式的否定式，请用支持集策略对其进行归结。

解：用支持集策略对其进行归结的过程如下。

①P∨Q

②￢P∨R

③￢Q∨R

④￢R

⑤￢P　　　　　②与④归结

⑥￢Q　　　　　③与④归结

⑦Q　　　　　　①与⑤归结

⑧P　　　　　　①与⑥归结

⑨R　　　　　　③与⑦归结

⑩NIL　　　　　⑥与⑦归结

（2）线性输入策略

线性输入策略对参加归结的子句做出了如下的限制：参加归结的两个子句中必须至少有一个是初始子句集中的子句。初始子句集是指最初给出要求进行归结的子句。

线性输入策略具有可限制归结式的数量、方法简单等优点。但是它是不完备的归结策略，即若子句集是不可满足的，则用线性归结策略有可能无法归结出空子句。

例3.21 对例3.20中的初始子句集S，用线性输入策略对其进行归结。

解：用线性输入策略对其进行归结的过程如下。

（1）P∨Q

（2）￢P∨R

（3）￢Q∨R

（4）￢R

（5）￢P　　　　　（2）与（4）归结

（6）￢Q　　　　　（3）与（4）归结

（7）Q　　　　　　（1）与（5）归结

（8）P　　　　　　（1）与（6）归结

（9）R　　　　　　（3）与（7）归结

（10）R　　　　　　（2）与（8）归结

（11）NIL（4）与（9）归结

（3）单文字子句策略

如果一个子句中只包含一个文字，则称它为单文字子句。

单文字子句策略要求参加归结的两个子句中至少有一个是单文字子句。使用该策略进行归结时，归结式比亲本子句含有较少的文字，向着空子句的方向前进，因此有较高的归结效率。单文字子句策略是不完备的，当初始子句集中不含有单文字子句时，使用该策略的推理就无法进行下去。

例3.22 设有子句集S={￢I（x）∨R（x），I（a），￢R（y）∨￢L（y），L（a）}，请用单文字子句策略对其进行归结。

解：用单文字子句策略对其进行归结的过程如下。

①￢I（x）∨R（x）

②I（a）

③￢R（y）∨￢L（y）

④L（a）

⑤R（a）　　　　　　①与②归结{a/x}

⑥￢R（a）　　　　　③与④归结{a/y}

⑦￢I（a）　　　　　①与⑤归结{a/x}

⑧￢L（a）　　　　　③与⑤归结{a/y}

⑨NIL　　　　　　　　⑤与⑥归结

（4）祖先过滤形策略

祖先过滤形策略要求参加归结的两个子句必须至少满足下列两个条件中的任何一个：

●C1与C2中至少有一个是初始子句集中的子句。

●如果有两个子句都不是初始子句集中的子句，则一个应是另一个的祖先。C1是子句C2的祖先是指C2是由C1与别的子句归结后得到的归结式。祖先过滤形策略是完备的归结策略。

例3.23 设有子句集：

S={￢P（x）∨Q（x），￢P（y）∨￢Q（y），P（u）∨Q（u），P（t）∨￢Q（t）}

请用祖先过滤形策略对其进行归结。

解：用祖先过滤形策略对其进行归结的过程如图3.5所示。

3.4.5 使用归结原理证明问题

归结原理给出了证明子句集不可满足的理论基础，对于证明公式由前提条件A1∧A2∧…∧An可推导出结论G，即证明A1∧A2∧…∧An→G是蕴涵式。

对这个蕴涵式的证明，我们可以将其转化成证明A1∧A2∧…∧An∧￢G是不可满足的。因此，应用归结原理对其子句集进行归结，若能归结出空子句，则可得证。

应用归结原理证明谓词公式的步骤如下：

（1）否定结论G，得到￢G。

（2）将前提条件A1∧A2∧…∧An和￢G化为子句集S。

（3）应用归结原理，反复对子句集S进行归结，若能归结出空子句，则证明子句集S的不可满足性。从而证明了公式A1∧A2∧…∧An→G为真。

例3.24 已知前提条件：

（∃x）（R（x）∧（∀y）（D（y）→L（x，y）））

（∀x）（R（x）→（∀y）（S（y）→￢L（x，y）））

试证明可推导出结论（∀x）（D（x）→￢S（x））。

证明：首先将前提条件和结论的否定式化为子句集。

①R（a）

②￢D（y）∨L（a，y）

③￢R（x）∨￢S（u）∨￢L（x，u）

④D（b）

⑤S（b）

⑥￢S（u）∨￢L（a，u）①与③归结{a/x}

⑦L（a，b）　　　　　　②与④归结{b/y}

⑧￢L（a，b）　　　　　⑤与⑥归结{b/u}

⑨NIL　　　　　　　　　⑦与⑧归结

例3.25 某公司招聘工作人员，A、B、C三人应试，经面试后公司表示如下想法：

①三人中至少录取一人。

②如果录取A而不录取B，则一定录取C。

③如果录取B，则一定录取C。

求证：公司一定录取C。

证明：谓词P（x）表示公司录取x。将已知条件表示如下：

①P（A）∨P（B）∨P（C）

②（P（A）∧￢P（B））→P（C）

③P（B）→P（C）

结论的否定式表示如下：

④￢P（C）

将上面四个公式化为子句集：

①P（A）∨P（B）∨P（C）

②￢P（A）∨P（B）∨P（C）

③￢P（B）∨P（C）

④￢P（C）

应用归结原理进行归结：

⑤P（B）∨P（C）①与②归结

⑥P（C）　　　　③与⑤归结

⑦NIL　　　　　　④与⑥归结

得证，公司一定录取C。

例3.26 已知如下事实：①Marcus是人。②Marcus是罗马人。③Caser是一位统治者。④所有罗马人或忠于Caser或仇恨他。⑤每个人都忠于某个人。⑥人们只想暗杀他们不忠于的统治者。⑦Marcus试图暗杀Caser。

求证：Marcus仇恨Caser。

证明：（1）首先定义谓词。

man（x）　　　　　　表示x是人

Roman（x）　　　　　表示x是罗马人

ruler（x）　　　　　表示x是统治者

loyal（x，y）　　　　表示x忠于y

hate（x，y）　　　　表示x仇恨y

tryassassinate（x，y）表示x试图暗杀y

（2）然后将已知事实用一阶谓词表示法表示。

man（Marcus）

Roman（Marcus）

ruler（Caser）

（∀x）（Roman（x）→loyal（x，Caser）∨hate（x，Caser））

（∀x）∃（y）loyal（x，y）

（∀x）∀（y）（man（x）∧ruler（y）∧tryassassinate（x，y）→￢loyal（x，y））

tryassassinate（Marcus，Caser）

结论：hate（Marcus，Caser）

（3）将已知事实和结论的否定式化为子句集。

1man（Marcus）

2Roman（Marcus）

3ruler（Caser）

4￢Roman（x）∨loyal（x，Caser）∨hate（x，Caser）

5loyal（y，f（y））

6￢man（u）∨￢ruler（v）∨￢tryassassinate（u，v）∨￢loyal（u，v）

7tryassassinate（Marcus，Caser）

8￢hate（Marcus，Caser）

（4）将子句集进行归结。

9loyal（Marcus，Caser）∨hate（Marcus，Caser）　　　2与4归结{Marcus/x}

10loyal（Marcus，Caser）　　　　　　　　　　　　　　　8与9归结

11￢ruler（v）∨￢tryassassinate（Marcus，v）∨￢loyal（Marcus，v）　　1与6归结{Marcus/u}

12￢tryassassinate（Marcus，Caser）∨￢loyal（Marcus，Caser）　　　3与11归结{Caser/v}

13￢loyal（Marcus，Caser）　　　　　7与12归结

14NIL10与13归结

得证Marcus仇恨Caser。

3.4.6 用归结原理求解问题

用归结原理求解问题的步骤如下：

（1）把已知前提条件用谓词公式表示出来，并且化为子句集S。

（2）把待求解的问题用谓词公式表示出来，然后将其否定，并与谓词公式ANSWER构成析取式，ANSWER是一个为求解问题而专设的谓词，并且其变元须与谓词公式的变元一致。

（3）将（2）中的析取式化为子句集，并且将该子句集并入子句集S中，得到子句集S′。

（4）对子句集S′应用归结原理进行归结。

（5）若得到归结式ANSWER，则答案就在ANSWER中。

3.27 已知下列事实：

①王喜欢吃所有种类的食物。

②苹果是食物。

③任何一个东西，若任何人吃了它都不会被害死，则该东西是食物。

④李吃花生且仍然活着。

求：王喜欢吃什么？

解：（1）定义谓词及个体。

Food（x）x是食物

Like（x，y）x喜欢吃y

Eat（x，y）x吃y

Alive（x）x活着

个体：王Wang 李Li 苹果Apple 花生Peanuts

（2）将已知事实用谓词公式表示。∀（x）（Food（x）→Like（Wang，x））Food（Apple）

∀（x）∀（y）（Eat（x，y）∧Alive（x）→Food（y））

Eat（Li，Peanuts）∧Alive（Li）

求解问题可表示为Like（Wang，u），其否定式与ANSWER的析取式为￢Like（Wang，u）∨ANSWER（u）。

（3）化为子句集。

1￢Food（x）∨Like（Wang，x）

2Food（Apple）

3￢Eat（y，z）∨Alive（y）∨Food（z）

4Eat（Li，Peanuts）

5Alive（Li）

6￢Like（Wang，u）∨ANSWER（u）

（4）将子句集进行归结。

7Like（Wang，Apple）　　1与2归结{Apple/x}

8ANSWER（Apple）　　6与7归结{Apple/u}

9￢Alive（Li）∨Food（Peanuts）　　3与4归结{Li/y，Peanuts/z}

10Food（Peanuts）　　　　5与9归结

10Like（Wang，Peanuts）　1与10归结{Peanuts/x}

12ANSWER（Peanuts）　　　6与11归结{Peanuts/u}得证：王喜欢吃苹果和花生。

例3.28 设A、B、C三人中有人从不说真话，也有人从不说假话，某人向这三人分别问同一个问题，谁是说谎者？A答“B和C是说谎者”；B答“A和C是说谎者”；C答“A和B中至少有一个是说谎者”。求谁是老实人。

解：T（x）表示x是说真话的人。

A说的是真话：T（A）→￢T（B）∧￢T（C）

A说的是假话：￢T（A）→T（B）∨T（C）

B说的是真话：T（B）→￢T（A）∧￢T（C）

B说的是假话：￢T（B）→T（A）∨T（C）

C说的是真话：T（C）→￢T（A）∨￢T（B）

C说的是假话：￢T（C）→T（A）∧T（B）

将以上各句化为子句集。

（1）￢T（A）∨￢T（B）

（2）￢T（A）∨￢T（C）

（3）T（A）∨T（B）∨T（C）

（4）￢T（B）∨￢T（C）

（5）￢T（C）∨￢T（A）∨￢T（B）

（6）T（C）∨T（A）

（7）T（C）∨T（B）

求解问题的否定式与ANSWER的析取式为：

（8）￢T（x）∨ANSWER（x）

（9）T（C）∨￢T（B）　（1）与（7）归结

（10）T（C）　　　（7）与（9）归结

（11）ANSWER（C）　　（8）与（10）归结{C/x}

所以，求得C是老实人。