演绎检索器示例

Question

在Lisp中，假设知识库中有以下两条规则：

(append nil ?x ?x)
(<- (append (cons ?x ?l1) ?l2 (cons ?x ?l3))
    (append ?l1 ?l2 ?l3))

那我怎么能推断如果我们问

(ask '(append (cons a (cons b nil))
              (cons c nil)
              ?l)
     '?l))

我们将得到结果'((cons a (cons b (cons c nil)))

这是我的Lisp类中的一个例子，希望你能帮助我理解这个检索器。谢谢。

Answer 1

要理解这个问题，我认为您首先需要掌握两个关键概念:反向链接和统一。

对于粗略的简化，以下是反向链接的工作原理:如果可以将目标(示例中“ask”的第一个参数)与任何规则的头部(请注意不确定性)统一起来，请尝试；如果可以，则将该规则的主体(可能为空)添加为子目标，并将统一的结果(一组变量绑定)存储起来。递归地将上述过程应用于具有累积绑定的每个子目标，直到(1)没有适用的规则，这意味着证明失败，或者(2)没有更多的子目标，这意味着证明成功。在后一种情况下，目标变量(第二个参数)的绑定将是答案。