Hints on Theorem Provers

This page gives some suggestions for implementing the Theorem Provers assignment. You are free to follow these hints, or to use other methods of your choice if you prefer.

A good technique in Lisp is to write program components and test them individually.

The backchaining prover is somewhat different from the resolution provers. It is not necessary to represent the not operator since we know the clauses are Horn clauses. It is useful to index clauses, e.g. by storing the clause on the property list of the first predicate name. Clauses could be represented as:
The last clause is interpreted as (GRANDPARENT X Y) is true if (PARENT Z Y) is true and (PARENT X Z) is true.

The backchaining programs should return a list of substitution sets, e.g.

(((X ZEUS)) ((X HERA)))
In this list, ((X ZEUS)) (equivalent to ((X . (ZEUS)) ) is one substitution set, containing a single substitution, and ((X HERA)) is a second substitution set.

The answer to a backchaining problem is the union of:

To backchain on a clause, the query should unify with the first predicate in the clause; this produces a substitution set. The substitutions must be made into the remaining predicates in the list, and each of them must be answered; as the process proceeds, more substitutions are produced.