归结原理由J.A.Robinson于1965年提出，又称为消解原理。该原理是Robinson在Herbrand理论基础上提出的一种基于逻辑的、采用反证法的推理方法。由于其理论上的完备性，归结原理成为机器定理证明的主要方法。

定理证明的实质就是要对给出的（已知的）前提和结论，证明此前提推导出该结论这一事实是永恒的真理。这是非常困难的，几乎是不可实现的。

要证明在一个论域上一个事件是永真的，就要证明在该域中的每一个点上该事实都成立。很显然，论域不可数时，该问题不可能解决。即使可数，如果该轮域是无限的，问题也无法简单地解决。

Herbrand采用了反证法的思想，将永真性的证明问题转化为不可满足性的证明问题。Herbrand理论为自动定理证明奠定了理论基础，而Robinson的归结原理使自动定理证明得以实现。因此，归结推理方法在人工智能推理方法中有着很重要的历史地位。

1）归结法的特点

归结法是与演绎法完全不同的新的逻辑演算算法。它是一阶逻辑中至今为止的最有效的半可判定的算法，也是最适合用计算机进行推理的逻辑演算方法。

半可判定即对一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定（证明其为永真式）。

2）归结法基本原理

归结法的基本原理是采用反证法（或者称为反演推理方法），将待证明的表达式（定理）转换成逻辑公式（谓词公式），然后进行归结，若归结能够顺利完成，则证明原公式（定理）是正确的。

逻辑可分为经典逻辑和非经典逻辑，其中经典逻辑包括命题逻辑和谓词逻辑。归结原理是一种主要基于谓词（逻辑）知识表示的推理方法，而命题逻辑是谓词逻辑的基础。因此，在讨论谓词逻辑之前，先讨论命题逻辑的归结，便于内容上的理解。

1.命题逻辑的归结法

设有由命题逻辑描述的命题A1，A2，A3和B，要求证明A1∧A2∧A3→B定理（重言式）。　

很显然，A1∧A2∧A3→B是重言式等价于A1∧A2∧A3∧¬B是矛盾（永假）式。归结推理方法就是从A1∧A2∧A3∧¬B出发，使用归结推理来寻找矛盾，最后证明定理A1∧A2∧A3→B的成立。这种方法可称作反演推理方法。

1）归结式的定义

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

例如：有子句：C1=P∨，C2=¬P∨存在互补对P和¬P，

则可得归结式：C12=C′1∨

下面证明归结式是原两子句的逻辑结果，或者说任一使C1、C2为真的解释I下必有归结式C12也为真。

证明：

设I是使C1，C2为真的任一解释，若I下的P为真，从而¬P为假，必有I下为真，故C12为真。若不然，在I下P为假，从而I下C′1为真，故I下C12为真。于是C1∧C2为真时，C1∧C2→R（C1，C2）成立。

注意：C1∧C2→C12，反之不一定成立。因为存在一个使∨为真的解释I，不妨设C′1为真，C′2为假，若P为真，则¬P∨C′2就为假了。

2）命题逻辑的归结法证明过程

命题逻辑的归结过程也就是推理过程。推理是根据一定的准则由称为前提条件的一些判断导出称为结论的另一些判断的思维过程。

命题逻辑归结方法的推理过程核心：把一阶命题逻辑公式：A1∧A2∧A3→B，转化成：A1∧A2∧A3∧¬B的形式。

步骤：

（1）先把问题写成：A1∧A2∧A3→B的形式，如图241所示。

图241　问题转化

（2）将合取范式写成集合表示形式，即子句集S。

其中子句是析取项，即A∨B，C∨D等形式。

例：P∧（Q∨R）∧（¬P∨¬Q）∧（P∨¬Q∨R）

S=｛P，Q∨R，¬P∨¬Q　P∨¬Q∨R｝

（3）归结式。设有两个子句C1=P∨，C2=¬P∨，从中消去互补对得到新子句　

称为C1和C2的归结式。

注意：没有互补对的两个子句没有归结式（形如¬P和P称互补对，即¬P∨P=I）。

（4）归结推理。对子句集S中的子句使用归结法进行归结，如果归结为空子句则证明成功，否则为失败。

［例］　证明（（P→Q）∧¬Q）→¬P

证明：

（1）将命题化成合取范式：

（2）建立子句集：S=｛¬P∨Q，¬Q，P｝

（3）对S进行归结：

①¬P∨Q

②¬Q

③P

④¬P　①×②归结

⑤□　③×④归结

归结过程如图2-42所示。

图2-42　归结过程

命题逻辑的归结方法小结：

（1）建立待归结命题公式。首先根据反证法将所求证的问题转化成命题公式，求证其是矛盾式（永假式）。

（2）求取合取范式。（3）建立子句集。

（4）归结。归结法是在子句集S的基础上通过归结推理规则得到的，归结过程的最基本单元是得到归结式的过程。从子句集S出发，对S的子句间使用归结推理规则，并将所得归结式仍放入到S中（注意：此过程使得子句集不断扩大，是造成计算爆炸的根本原因），进而再对新子句集使用归结推理规则。重复使用这些规则直到得到空子句。这便说明S是不可满足的，从而与S所对应的定理是成立的。归结步骤：

①对子句集中的子句使用归结规则。

②归结式作为新子句加入子句集参加归结。

③归结式为空子句NULL为止。

得到空子句NULL，表示S是不可满足的（矛盾），故原命题成立。

2.谓词逻辑归结方法

由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以在生成子句集之前要对逻辑公式作处理。具体地说，就是将其转化为Skolem标准形，然后在子句集的基础上进行归结。虽然归结的基本方法都相同，但是其过程较命题公式的归结过程复杂得多。

以前面的谓词演算和命题归结为基础，给出谓词逻辑的归结方法。

（1）问题化成谓词逻辑公式。即根据反证法将所求证的问题转化成为谓词公式，求证其是矛盾式（永假式）。

（2）谓词逻辑公式化成前束范式。

（3）前束范式化成合取范式。

（4）消存在量词和“→”。

（5）写出子句集。

（6）用归结方法进行归结，在此步中用置换因子进行合一归结。

［例1］　死狗问题。

命题：fido is a dog，all dogs are animals，all animals will die.

证明：fido will die.

证明：

（1）先将问题化成谓词演算公式：

①All dogs are animals：∀（x）（dog（x）→animal（x））

②Fido is a dog：dog（fido）

③｛fido/x｝→animal（fido）

④all animals will die：∀（y）（animal（y）→die（y））

⑤｛fido/y｝→die（fido）

（2）把谓词演算公式化成子句集：

①¬dog（x）∨animal（x）

②dog（fido）

③¬animal（y）∨die（y）

④¬die（fido）　（目标取反）

（3）用归结原理证明（见图2-43）。

图2-43　“死狗问题”的归结证明过程

［例2］　“幸运学生”的故事。

任何通过了考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有考试，John不学习但很幸运，任何人只要是幸运的就可以中彩。John快乐吗？

证明：

（1）把这些句子变成谓词形式：

任何通过考试并中了彩票的人是快乐的：

∀x（pass（x，history）∧Win（x，lottery）→happy（x））

任何肯学习的人或幸运的人可以通过考试：

∀x∀y（Study（x）∨lucky（x）→pass（x，y））

John不学习但幸运：

¬study（John）∧Lucky（John）

幸运的人中彩票：

∀x（Lucky（x）→Win（x，lottery））

（2）将上述命题公式转化成子句形式：

①¬pass（x，history）∨¬win（x，lottery）∨happy（x）

②¬study（x）∨pass（x，y）

③¬lucky（x）∨Pass（x，y）

④¬study（John）

⑤Lucky（John）

⑥¬lucky（x）∨win（x，lottery）

⑦¬happy（John）（目标的否定）

（3）用归结原理进行证明（见图2-44）。

图2-44　“幸运学生”问题的归结证明过程

由上面的证明过程可知，John是快乐的。

［例3］　激动人心的故事问题。

假设所有不贫穷，并且聪明的人是快乐的。那些看书的人是聪明的。John能看书并且不贫穷，快乐的人过着激动人心的生活。你能发现谁过着激动人心的生活吗？

证明：

（1）把上述故事翻译成谓词演算表达式：

否定目标是：

（2）写出子句集形式：

（3）用归结原理进行归结证明（见图2-45）。

由此可知，John过着激动人心的生活。

3.归结策略和简化技术

图2-45　“激动人心的故事”问题的归结证明过程

从上面的几个例子中可以发现，在子句集S=｛a1，…，an｝的子句中，并没有规定a1，…，an之间的顺序，在那里是随机地用两个子句ai，aj来进行归结，由此可以看出，在选择ai与aj时就有n（n－1）种组合方法，依此类推，在选择另一个子句时则有n－2种组合方法，当把该式归结完时则所选子句的方法有：n（n－1）（n－2）…（n－m）种，用了m步归结完，则有O（nm），n≥2，m≥2。这样则出现了组合爆炸情况，为避免这种现象出现，必须研究归结策略，找出一种尽量不产生组合爆炸的归结方法。

原则：在S=｛a1，a2，…，an，¬m｝中，主要研究S1=｛a1，a2，…，an｝和S2=｛¬m｝，看怎样组合更有优势，即S=S1∪S2。

在描述这些策略之前，先作一些说明：

（1）一个子句集如果不存在一个解释可以确定该子句集为可满足的，则称之为不可满足的，即

若S=｛a1，…，an，¬m｝→可满足，则S′=｛a1，…，an，m｝→不可满足。

也就是若（a1∧…∧an∧¬m）为可满足的，则（a1∧…∧an∧m）为不可满足的。

（2）如果给定一个不可满足的子句集合，通过单纯使用某个推理规则可以确定其不可满足性，则称该推理规则是否证完备的。

（3）一个策略是完备的，如果只要一个子句集合是不可满足的，则用该策略加上否证完备推理规则，可以保证发现一个否证。

分析我们原来使用的归结证明：

目的证明公式：A→B⇔¬A∨B

归结证明思想，如图2-46所示。

下面介绍几种归结策略。

1）广度优先策略

原理：子句集S=｛a1，…，an，¬m｝中的任何子句ai在第一轮都要和其他子句进行归结，此时可得子句S1=｛a′1，…，a′m｝；在第二轮归结时，将第一轮产生的新子句S1，加入原子句集进行归结；在第n轮归结时，将先前所有产生的子句加到原始子句进行归结S′n，即，S′=｛S1，S2，…，Sn｝。

图2-46　归结证明的基本思想

优点：

（1）该策略能保证找到最短归结路径。

（2）该策略是一种完备的策略（见图2-47）。

图2-47　广度优先归结策略

2）支持集策略

原理：对于一组输入子句集S，可以指定S的一个子集T，称T为支持集，这个策略要求每次归结结果要在支持集中有一个祖先，也就是说，支持集使得归结作用的两个子句中至少一个或是否定目标式，或是一个在目标式上产生的归结结果子句。

即：如果S是不满足的，并且S－T是满足的，那么T是不可满足的，并且（S－T）∧T也是不可满足的。

3）单位优先策略

原理：用一个只有一个子句的项进行归结，如图2-48所示。

图2-48　单位优先归结策略

4）线性输入形式策略

原理：直接用否定目标和原始公理，对否定目标和一个公理进行归结得到一个新子句，这个结果子句再和一个公理归结得到另一个新子句，该新子句又和公理归结，这个过程一直持续到空子句出现。

5）从归结否证中提取答案

方法：

①保留目标的原始结论。

②归结原式中的合一因子。(www.daowen.com)

③用归结式中的合一因子替代原目标式中的变元，直到归结完，最后便得其答案。

问题：计算机在归结证明时要用额外的指针

［例］　Fido问题

狗Fido无论主人John走到哪里都跟到哪里。John在图书馆，Fido在哪里？

解：

（1）将原式翻译成谓词：

at（John，x）→at（Fido，x）

at（John，Library）

at（Fido，z）（目标）

（2）子句：

①¬at（John，x）∨at（Fido，x）

②at（John，Library）

③¬at（Fido，z）（目标否定）

回答是：Fido在图书馆。求解过程如图2-49所示。

图2-49　Fido问题的求解

4.规则演绎系统

在人工智能系统中，谓词逻辑公式常可用来表示各种知识。通常很多应用知识是用蕴涵形式直接表达的，因此都带有超逻辑的或启发式的控制信息。而子句形表示只给出了谓词间的逻辑关系。在归结反演证明系统中，要把这些表达式化成子句表示，这就可能丢失包含在蕴涵形中有用的控制信息。因此，有时候会希望系统能按近于原始给定的描述形式来使用这些公式，不把它们都化成子句集，这就是基于规则演绎系统的基本思想。

一般情况下，表述有关问题的知识分两类：规则和事实。规则公式由蕴含形给出的若干语句组成（形如A1∧A2∧…∧An→B或if A1∧A2∧…∧Anthen B），表示某一特定领域中的一般知识，并可以当作产生式规则来使用。事实公式则是不含蕴含符号的谓词公式，表示该问题领域的专门知识。本节讨论的演绎系统就是根据这些事实和规则来证明一个目标公式，这种定理证明系统是直接法的证明系统而不是反演系统。一个直接系统不一定比反演系统更有效，但其演绎过程容易为人们所理解。这类系统主要强调使用规则进行演绎，故称为基于规则的演绎系统。

1）规则正向演绎系统

（1）事实表达式的与或形变换。在基于规则的正向演绎（Forward chaining）系统中，把事实表示为非蕴含形式的与或形作为系统的总数据库。注意这些事实不要化为子句型，只要是谓词公式即可。

把一个公式化成与或形的步骤如下：

①利用W1→W2和（¬W1∨W2）的等价关系，消去“→”。

②利用德·摩根律把否定符号移进括号内，直到每个否定符号的辖域最多只含有一个谓词为止。

③对所得的表达式进行Skolem化和前束化。

④对全称量词辖域内的变量进行改名和变量标准化，而存在量词的约束变量用Skolem函数代替。

⑤删去全称量词。

例如：事实表达式

把它化为Q（V，A）∧｛［¬R（V）∧¬P（V）∨¬S（A，V）］｝

对变量更名标准化，使得同一变量不出现在事实表达式的不同合取式中，更名后得到表达式Q（W，A）∧｛［¬R（V）∧¬P（V）］∨¬S（A，V）｝

注意：Q（V，A）中的变量V可用新变量W代替，而合取式［¬R（V）∧¬P（V）］中的变量V却不可更名，因为它在后面也出现在析取式¬S（A，V）中。

（2）事实表达式的与/或图表示。

①事实表达式（E1∨…∨Ek）的析取关系子表达式E1，…，Ek是用后继节点表示的，并由一个k线连接符把它们连接到父辈节点上，如图2-50所示。

②某个事实表达式（E1∧…∧Ek）的每个合取子表达式E1，E2，…，Ek是由单一的后继节点表示的，并由一个单线连接符接到父辈节点，如图2-51所示。

图2-50　正向演绎系统的析取关系与/或图　

图2-51　正向演绎系统的合取关系与/或图

上例也可用图2-52表示。

图2-52　一个事实表达式的与或树表示

由此得到的子句为

（3）与/或图的F规则变换。规则的标准形是L→W。其中L是单文字（单项），W为与或形的唯一公式。变换规则是：先把这些变量的量词局部地调换到前项，再把全部存在量词Skolem化。下面举例说明：

［例］　规则（∀x）｛［（∃y）（∀Z）P（x，y，Z）］→（∀u）Q（x，u）｝可以通过下列步骤加以变换。

①暂时消去蕴含符号：

②把否定符号移进第一个析取式中，调整变量的量词；

③进行Skolem化；

④把所有全称量词移到前面然后消去；

⑤恢复蕴含式。

［例］　如图2-53所示，若用规则S→（X∧Y）∨z进行匹配（黑色粗箭头表示匹配弧），则得图2-54。

由图2-53可见：［（P∨Q）∧R］∨［S∧（T∨V）］的子句集为

图2-53　不含变量的与/或图

图2-54　应用一条L→W规则得到的与/或图

由图2-54可知，S→［（X∧Y）∨Z］的子句形为

应用两个规则子句中任一个对上述子句形中的S进行消解（见图2-55）。

图2-55　消解过程

于是得到四个子句对S进行消解式的完备集为

这些消解式全部包含在图2-54中。

（4）作为终止条件的目标公式。一个基于规则的正向演绎系统，其演绎过程就是不断地调用匹配上的规则对与/或图进行变换，直到生成的与/或图含有目标表达式为止，也就是要用目标公式作为系统的结束条件。正向系统的目标表达式要限制为文字析取形（子句形）的一类公式。当目标公式中有一个文字同与/或图中某一个端节点所标记的文字匹配上时，和规则匹配时的做法一样，通过匹配弧把目标文字添加到图上。这个匹配弧的后裔节点称为目标节点。这样，当产生式系统演绎得到的与/或图包含目标节点的解图时，系统结束演绎，这时便推出了一个与目标有关的子句。

下面举例说明系统的推理过程。

［例1］

事实：A∨B

规则：A→（C∧D），B→（E∧G）

目标：C∨G

在该例中，经过两次规则变换后，得到如图2-56所示的与/或图。其中一个解图的叶节点是C和G，分别与目标表达式C∨G中的文字C和G匹配，说明目标C∨G是该问题的逻辑推论，从而证明目标公式成立。

图2-56　满足终止条件的与/或图

图2-57　归结证明树

值得注意的是，只要求解图的叶节点全部与目标公式中的文字匹配上，并不要求目标公式中的每一个文字都必须与解图中的一个叶节点匹配。在该例中，即便是目标公式变为C∨G∨P∨Q，同样也可以推出目标公式成立，因为已经逻辑推导出C∨G成立。C∨G∨P∨Q只是在C∨G上又“或”上了两个命题，如果C∨G成立，C∨G∨P∨Q当然也成立，归结证明树如图2-57所示。

［例2］

事实与或形表示P（x，y）∨（Q（x，A）∧R（B，y））

规则蕴涵式P（A，B）→（S（A）∨X（B））

图2-58是这个例子应用规则变换后得到的与/或图，它有两个解图，对应的两个子句是

它们正是事实和规则公式组成的子句集对文字P进行归结时得到的归结式。

图2-58　应用一条含有变量的规则后得到的与/或图

一个解图是否是一致的，需要看该解图所涉及的若干个置换组成的置换集是否存在矛盾。当置换集没有矛盾存在时，称该置换集是一致的，否则就是不一致的。只有当解图所涉及的置换集是一致时，解图才是一致的。置换集一致的充分必要条件是该置换集存在合一复合。置换集的合一复合也是一个置换，表示的是置换集中所有置换“综合”以后的结果。

求一个置换集的合一复合，首先构造U1、U2两个表达式，其中U1由置换集中的所有被置换的变量组成，U2由与U1中的变量所对应的置换项组成。当U1、U2可以合一时，则所对应的置换集是一致的（一致置换），它们的mgu就是该置换集的合一复合。

合一复合是可结合、可交换的。这是一个很好的性质，说明在用基于规则的正向演绎方法求解问题时，与使用规则的次序无关。

当一个与/或图应用了好几条规则之后，推出的与/或图将含有多个匹配弧，这时任一解图可能有多于一个的匹配弧（对应的置换是u1，u2，…），因此在列写解图的子句集时，只考虑具有一致的匹配弧置换的那些解图（一致解图）。一个一致解图表示的子句是对得到的文字析取式应用一个合一复合的置换之后所得到的。

置换的一致集和置换的合一复合这两个概念定义如下：设有一个置换集｛u1，u2，…，un｝，其中ui=｛ti1／vi1，…，tim|i）／vim|i）｝是置换对集合，t是项，v是变量。

根据这个置换集，再定义两个表达式：

置换（u1，…，un）称为一致的，当且仅当U1和U2是可合一的。（u1，…，un）的合一复合（unifying composition）u是U1和U2的最一般的合一者。表2-1给出几个合一复合结果的实例。

表2-1　合一复合结果实例

可以证明，对一个置换集求合一复合的运算是可结合和可交换的（求置换的合成是不可交换的）。因此，一个解图对应的合一复合不依赖于构造这个解图时所产生的匹配弧的次序。再强调一下，我们要求一个解图具有一个一致匹配弧的置换集，这样，该解图所对应的子句才是从初始事实表达式和规则公式集推出的子句。

有时演绎过程会多次调用同一条规则，这时要注意每次应用都要使用改名的变量，以免匹配过程产生一些不必要的约束。此外，也可多次使用同一目标文字来建立多个目标节点，这也要采用改名的变量。

2）规则逆向演绎系统

基于规则的逆向演绎（Backward chaining）系统，其操作过程与正向演绎系统相反，是从目标到事实的操作过程，从then到if的推理过程。

（1）目标表达式的与或形式。

①采用与变换事实表达式同样的过程，把目标公式化成与或形，即消去符号“→”，把否定符号移进符号内。

②对全称量词Skolem化，并删去存在量词。

③与或形的目标公式与/或图表示。

在用与/或图表示目标表达式时，规定子表达式间的析取用单线连接符连接，即表示为“或”的关系，而子表达式的合取用k -连接符连接，即表示为“与”的关系。也就是说，目标表达式中的“与”“或”关系，和与/或图中的“与”“或”关系是一致的。这与正向系统中对事实表达式的与/或图表示是不一样的。这一点可以这样来理解：对于目标来说，两个子表达式间如果是析取的话，则表示只要其中一个成立则目标成立，因此在与/或图中用“或”关系表示；如果子表达式间是合取的话，则必须每一个子表达式都成立，目标才能成立，所以在与/或图中用“与”关系表示。

目标表达式（E1∨E2∨…∨En）可用图2-59表示。

目标表达式（E1∧E2∧…∧En）可用图2-60表示。

图2-59　逆向演绎系统的析取关系与/或图

图2-60　逆向演绎系统的合取关系与/或图

［例］　目标表达式

被化成与或形：

式中f（y）为Skolem函数。

对目标的主要析取式中的变量标准化可得

注意：不能对析取的子表达式内的变量y改名而使每个析取式具有不同的变量。

该例的与/或图如图2-61所示。

图2-61　一个目标公式的与/或图

从这个目标公式可得子句集如下：

可见目标子句是文字的合取，而这些子句的析取是目标公式。

（2）与/或图的B规则变换。逆向系统中的B规则限制为W→L的形式，其中前项W是任意形式的与或形公式，后项L是单文字，蕴涵式的任何变量都受全称量词约束。当B规则为W→L1∧L2时，可化简为两条规则W→L1和W→L2来处理。

当与/或图中有某个端点的文字和L可合一且mgu为u时，B规则可应用，通过匹配弧连接的后裔节点L，就是规则前项W对应的与/或图表示的根节点。规则应用后得到的解图集所对应的子句就是对偶系统归结时得到的归结式集。即将规则W→L的否定式（W∧¬L）得到的子句和目标公式的子句一起，对文字L进行归结得到的归结式。

在逆向系统中，事实表达式限定为是文字的合取，并且进行了普通的Skolem化简，变量受全称量词约束。

（3）作为终止条件的事实节点的一致解图。逆向系统中的事实表达式均限制为文字和取形，它可以表示为一个文字集。当一个事实文字和标在该图文字节点上的文字相匹配时，就可以把相应的后裔事实节点添加到该与/或图中去。这个事实节点通过标有mgu的匹配弧与匹配的子目标文字节点连接起来。同一个事实文字可以多次重复使用（每次用不同变量），以便建立多重事实节点。

逆向系统演绎过程的结束条件是生成的与/或图含有事实表达式，而事实表达式限制为文字的合取形式。当事实表达式有一个文字同与/或图中某一个端节点所标记的文字（子目标）匹配上时，就可以通过匹配弧把事实文字加到图上。这样当最后得到的与/或图包含一个结束在事实节点上的一致解图时，系统便结束演绎。一个一致解图是解图中匹配弧置换集具有合一复合置换的那个解图。和正向系统类似，B规则可以多次调用，事实文字也可以多次匹配，但每次匹配都要进行变量改名。

下面通过一个简例说明逆向系统的演绎过程。

设事实有：

规则集：

询问：

If there are a cat and a dog such that the cat is unafraid of the dog.

目标公式：

图2-62是一个逆向系统的例子。同在正向系统中一样，黑色粗的箭头是匹配弧，它表示与/或图中的一个节点与某规则的结论部分匹配。同样，箭头的方向并不代表合一的“方向”，合一完全按照通常的合一原则进行。如图中左边Cat（x）与规则R5的Cat（x5）合一，图中的置换是｛x/x5｝，该置换作用于规则RR5的前提部分，Meows（x5）变换为Meows（x）。由于x和x5都是变量，所以置换也可以是｛x5/x｝。该置换作用于规则RR5的前提部分，Meows（x5）保持不变。在Meows（x5）与事实Meows（Myrtle）匹配时，置换变成了｛Myrtle/x5｝。此时由于Myrtle是常量，置换只能是｛Myrtle/x5｝。该局部图如图2-63所示。

图2-62　逆向系统的一致解图

图2-63　局部图　

由于置换不一样了，该局部图与原图有所变化，但是最终得到的合一复合是一样的。

图2-62给出这个问题逆向求解的一个一致解图，规则的应用由规则编号标记。解图中的所有匹配弧的置换集是：｛x/x5｝，｛Myrtle/x｝，｛Fido/y｝，｛x/y2，y/x2｝，｛Fido/y｝，｛y/x｝，｛Fido/y｝，｛Fido/y｝

由此求得的合一复合是：｛Myrtle/x5，Myrtle/x，Fido/y，Myrtle/y，Fido/x2，Fido/x1｝

解图是一个一致解图，目标公式得到证明。把这个合一复合置换应用到目标公式得到的，其回答语句为

（Cat（Myrtle）∧Dog（Fido）∧¬Afraid（Myrtle，Fido））

3）正向系统和逆向系统的比较和不相同的部分，以免在使用时混淆。

虽然正向系统中的规则和目标公式以及逆向系统的事实公式和规则都有限制，但它们仍然可以适用于许多情况。我们还可以把正向和逆向的推理结合在一起，建立基于规则的双向演绎系统。这样可减少使用的限制，但在处理结束条件以及F规则和B规则的选取策略方面比较复杂，这方面的问题可参阅有关文献。

表2-2　正向系统和逆向系统的比较