反向链接算法

9.4.1 反向链接算法

图9.6显示了一个简单的反向链接算法，FOL-BC-ASK。它用只包含单个元素（即原始查询）的目标列表来调用，并返回满足查询的所有置换的集合。目标列表可以认为是一个等待处理的“栈”；如果所有的栈内目标都可以得到满足，则当前的证明分支是成功的。算法选取列表中的第一个目标，在知识库中寻找正文字（或称为头）能与该目标合一的每个子句。每个这样的子句创建一个新的递归调用，在该递归过程中，子句的前提（或称为体）都被加入到目标栈内。记住事实就是只有头没有体的子句，因此当目标和某个已知事实合一时，不会有新的子目标添加到栈里，目标也就得到了解决。图 9.7 是从语句（9.3）到（9.10）得到Criminal(West)的证明树。

该算法采用置换的合成。COMPOSE(θ1, θ2)是个置换，其效果与依次应用每个置换的效果完全相同。也就是，

SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p))

在该算法中，存储在θ 中的当前变量绑定和用目标与子句头合一得到的绑定进行合成，给出用于递归调用的当前绑定的新集合。

图9.6 一个简单的反向链接算法

图9.7 为了证明West是个罪犯而由反向链接构造的证明树。阅读这棵树的方法是深度优先，从左到右。为了证明Criminal(West)，我们必须证明下面的4个合取子句。其中一些在知识库中，另一些则需要进一步的反向链接。每个成功合一的绑定显示在相应的子目标旁边。注意，一旦合取式中的某个子目标得以成功实现，它的置换就可以用于后续子目标。因此，当FOL-BC-ASK到达最后一个合取子句时，即原来Hostile(z)时，z已经被限制为Nono

反向链接，如同我们前面所写，显然是深度优先搜索算法。这意味它的空间需求与证明的规模成线性关系（目前，忽略存储答案所需的空间）。它还意味着反向链接（不像前向链接）要忍受重复状态和不完备性问题的困扰。我们将讨论这些问题和一些潜在的解决方案，但是我们首先来看看反向链接怎样应用于逻辑程序设计系统。