CS 381K: Theorem Provers
Due: November 7, 2007.
For this assignment, you are to write several variations of resolution
theorem provers in Lisp, and a backchaining theorem prover.
- Representation: Use an array of pointers
to contain the set of clauses.
Initially, it will contain the premise clauses, followed by clauses
derived from the negated conclusion. As resolvents are generated from
these clauses, they are added to the end.
Each literal will be of the form: (predicate term ... term) .
An atomic term is considered to be a variable; a non-atomic term must
be a function of the form: (function term ... term) .
A constant is represented as a function of no arguments: (JOHN).
Negated literals use a not operator.
The notation does not contain any symbols for quantifiers or logical
connectives; these, and the meanings of symbols, are determined
implicitly by the positions of elements in the list structures. The
input to your program will be clauses written in this syntax. For
example, the clauses representing the statements `All hounds howl' and
`John has either a cat or a hound' would be written:
( ( (NOT (HOUND X)) (HOWL X) )
( (HAVE (JOHN) (A)) )
( (CAT (A)) (HOUND (A)) ) )
For simplicity, you may assume that the sets of symbols used as
predicate names, function names, and variable names are disjoint in any
- Print out each input clause and each clause that is produced by
resolution; number the printed clauses and show the numbers of the
clauses from which they are derived. (More than one resolution of a
given pair of clauses may be possible.)
- A unification algorithm is provided in the file
sunifyb.lsp . The clauses must first be rewritten so that
they have no variables in common; a function separate is
provided to do this. The "hounds" clauses and some useful code
are provided in the file hounds.lsp .
- Use the two-pointer method to select pairs of clauses for
resolution; initialize the pointers so that you will be using the
set-of-support strategy. This can be done in the following way:
The "two-pointer method" is a breadth-first method that generates
many duplicate clauses.
- Initialize: Set the "inner loop" pointer to the front of the
list of clauses. Set the "outer loop" pointer to the first clause
resulting from the negated conclusion.
- Resolve: If the clauses denoted by the two pointers can be
resolved, produce the resolvent. Add the resolvent to the end of the
list of clauses and print it out. (Note: There may be more than one
possible resolvent from a pair of clauses. It may be advantageous to
check whether the resolvent is already present in the list of clauses;
while a full equivalence test is somewhat complex, even an
equal test is useful.) If the resolvent is empty ("box"),
stop; the theorem is proved.
- Step: Move the "inner loop" pointer forward one clause. If the
"inner loop" pointer has not reached the "outer loop" pointer, go
to the Resolve step. Otherwise, reset the "inner loop" pointer to
the front of the list of clauses and move the "outer loop" pointer
forward one clause. If the "outer loop" pointer goes beyond the
last clause in the list, stop; the theorem cannot be proved.
- Use the "hounds" problem as a test problem.
- Implement linear resolution, in which one resolvent is the last
clause produced. Test it and compare to the other methods. Linear
resolution is a depth-first method. Linear resolution may get stuck, in
which case it is necessary to back up to a previous clause (and the state
of trying resolvents with that clause) and proceed from that point.
- Implement unit preference, in which preference is given to resolving
unit clauses (or shorter clauses). We will allow some flexibility in
the definition of "unit preference".
Test it and compare to the other methods.
- Write a backchaining prover for use with Horn clauses (clauses that
have at most one positive literal). In backchaining, the positive literal
may be considered to be a conclusion (or program name), and the negative
literals may be considered to be subgoals (or subprograms). Look for
ground clauses that satisfy a goal first, then look for rules.
Use the following test problem:
Father(Zeus, Ares) <-
Mother(Hera, Ares) <-
Parent(x, y) <- Mother(x, y)
Parent(x, y) <- Father(x, y)
Grandparent(x, y) <- Parent(x, z), Parent(z, y)
<- Grandparent(x, Harmonia)
- Can backchaining solve the "hounds" problem? Explain.