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.

Functions are provided in the file hounds.lsp to maintain and print an array of clauses. Each clause has a number, and access by clause number is fast.
(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.
To resolve two clauses: (resolve n1 n2) where n1 and n2 are clause numbers.
1. Separate the two clauses so that they have no variables in common:
```
(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 .
2. Write two nested loops to look for literals that might be resolved: (P ...) in one clause and (NOT (P ...)) in the other clause. These loops should run to completion, since more than one resolution of two clauses may be possible.
3. If two such literals are found, see if the two literals unify. If so, this produces a list of substitutions, subs.
4. Make the result clause, e.g.,
```
(sublis subs (append (remove lit1 clause1)
                     (remove lit2 clause2)))
```
5. Add the new clause to the array of clauses using putclause.
6. Carefully test these components before proceeding.
The two-pointer method is easy: simply write two loops.
1. Outer loop: Start n2 with the number of the first conclusion clause.
2. Inner loop: Start n1 with 1 and continue up to n2.
resolve the clauses denoted by n1 and n2. Stop if "box", i.e. NIL, is produced.
Linear resolution requires that one clause be the result of the last resolution step. This is basically recursive depth-first search.
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.
Unit preference attempts to resolve unit clauses (more generally, shorter clauses). It is somewhat like the two-pointer method in the sense that the program should repeatedly choose two clauses and try to resolve them. The choice should be made so that unit (or shorter) clauses are resolved when possible.

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:

((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:

Ground instances that unify with the query, e.g. the query (FATHER X (ARES)) unifies with the ground clause (FATHER (ZEUS) (ARES)), with substitutions ((X ZEUS)).
Results from backchaining.

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.