4.2.3 规则双向演绎系统
　　在上两节中我们所讨论的基于规则的正向演绎系统和逆向演绎系统都具有局限性。正向演绎系统能够处理任意形式的if表达式，但被限制在then表达式为由文字析取组成的一些表达式。逆向演绎系统能够处理任意形式的then表达式，但被限制在if表达式为文字合取组成的一些表达式。我们希望能够构成一个组合的系统，使它具有正向和逆向两系统的优点，以求克服各自的缺点(局限性)。这个系统就是本节要研究的双向(正向和逆向)组合演绎系统。正向和逆向组合系统是建立在两个系统相结合的基础上的。此组合系统的总数据库由表示目标和表示事实的两个与或图结构组成。这些与或图最初用来表示给出的事实和目标的某些表达式集合，现在这些表达式的形式不受约束。这些与或图结构分别用正向系统的F规则和逆向系统的B规则来修正。设计者必须决定哪些规则用来处理事实图以及哪些规则用来处理目标图。尽管我们的新系统在修正由两部分构成的数据库时实际上只沿一个方向进行，但是我们仍然把这些规则分别称为F规则和B规则。我们继续限制F规则为单文字前项和B规则为单文字后项。
组合演绎系统的主要复杂之处在于其终止条件，终止涉及两个图结构之间的适当交接处。这些结构可由标有合一文字的节点上的匹配棱线来连接。我们是用对应的mgu来标记匹配棱线的。对于初始图，事实图和目标图间的匹配棱线必须在叶节点之间。当用F规则和B规则对图进行扩展之后，匹配就可以出现在任何文字节点上。
　　在完成两个图间的所有可能匹配之后，目标图中根节点上的表达式是否已经根据事实图中根节点上的表达式和规则得到证明的问题仍然需要判定。只有当我们求得这样的一个证明时，证明过程才算成功地终止。当然，当我们能够断定在给定方法限度内找不到证明时过程则以失败告终。
　　一个简单的终止条件是某个判定与或图根节点是否为可解过程的直接归纳。这个终止条件是建立在事实节点和目标节点间一种叫做CANCEL的对称关系的基础上的。CANCEL的递归定义如下：
　　定义：如果(n,m)中有一个为事实节点，另一个为目标节点，而且如果n和m都由可合一的文字所标记，或者n有个外向k线连接符接至一个后继节点集{Si}使得对此集的每个元CANCEL(Si,m)都成立，那么就称这两节点n和m互相CANCEL(即互相抵消)。
　　当事实图的根节点和目标图的根节点互相CANCEL时，我们得到一个候补解。在事实和目标图内证明该目标根节点和事实根节点互相CANCEL的图结构叫做候补CANCEL图。如果候补CANCEL图中所有匹配的mgu都是一致的，那么这个候补解就是一个实际解。
　　下面我们举例说明图4.9中的初始事实图和初始目标图间的匹配。图中用