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.
(putclause clause n1 n2) increments the clause number, adds a new clause, and prints the clause with the numbers of its source clauses n1 and n2 (if specified).
It may be useful to modify putclause ignore duplicate clauses. Although a careful test for duplicate clauses is nontrivial, even the equal test will remove some duplicates.
(setq clause1 (sublis (separatecl clause1 clause2) clause1))For example, if the clauses are ( (not (p x)) (q x) ) and ( (not (q x)) (r x) ), change the first clause to ( (not (p T17)) (q T17) ). separate is defined in the file sunifyb.lsp .
(sublis subs (append (remove lit1 clause1) (remove lit2 clause2)))
Initialize, then call the depth-first search function with first conclusion clause number as the "last" clause.
In the recursive function, given the number of the last clause, try to resolve that clause with each existing clause. If it works and produces "box", i.e. NIL, return 'proved . Otherwise, try calling the recursive function with each of the clauses resulting from the resolution.
((FATHER (ZEUS) (ARES))) ((GRANDPARENT X Y) (PARENT Z Y) (PARENT X Z))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.