Go backward to 4 Unification
Go up to Top

5 Proofs (with variables)

Consider the following knowledge base:

ap(emp,L,L).
ap(c(H,T),L,c(H,R)) <-
   ap(T,L,R).
adj(A,B,L) <-
   ap(F,c(A,c(B,E)),L).

Give a top down derivation (including all substitutions) for one answer to the query:
```
? adj(b,Y,c(a,c(b,c(b,c(a,emp))))).
```
Are there any other answers? If so, explain where a different choice could be made in the derivation in the previous answer, and continue the derivation showing another example. If there are no other answers explain why not.

[You are meant to do this exercise as would a computer, without knowing what the symbols mean. If you want to give a meaning to this program, you could read ap as append, c as cons, emp as empty, and adj as adjacent.]

Solution to part (a)

Solution to part (b)