Deductive Retriever Example

Question

In Lisp, suppose I have these two rules in the knowledge base:

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

Then how could I infer that if we ask

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

we will get the result '((cons a (cons b (cons c nil)))?

This is one example from my Lisp class, I hope you could help me understand this retriever. Thank you.

Answer 1

To understand the problem, I think you'll need to acquire two key concepts first: backward chaining and unification.

With gross simplification, here is how backward chaining works: try if it is possible to unify the goal (the first argument for 'ask' in your example) with the head of any of the rules (note the nondeterminism); if yes, add the body (which may be empty) of that rule as subgoals and stash the result of unification (a set of variable bindings). Recursively apply the above procedure to each subgoal with the accumulated bindings until either (1) there is no applicable rule, which means the proof fails, or (2) there is no more subgoal, which means the proof succeeds. In the latter case, the binding of the target variable (second argument) would be the answer.