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.

1. 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 given problem.
2. 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.)
3. 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 .
4. 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:
   1. 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.
   2. 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.
   3. 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.
   The "two-pointer method" is a breadth-first method that generates many duplicate clauses.
5. Use the "hounds" problem as a test problem.
6. 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.
7. 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.
8. 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)    <-
   Father(Ares,Harmonia) <-
   Parent(x, y)          <- Mother(x, y)
   Parent(x, y)          <- Father(x, y)
   Grandparent(x, y)     <- Parent(x, z), Parent(z, y)
                         <- Grandparent(x, Harmonia)
                               [negated question]
   

9. Can backchaining solve the "hounds" problem? Explain.