Progress Report for Independent Study                 Oct. 22, 1991

Dr. Slagle,

  I have made the changes you suggested to the proposal.  I sent you the
revised proposal in a separate note.

  In your comments, you had a question mark about bound variables.  I wrote
"If a variable is bound it points to a literal or another bound variable."
I understand why this is not correct.  A variable can be bound to a term
within a literal, but not an entire literal (in first order logic).  In my
program I am using the same data structure to represent a literal or a term.
It includes a pointer to a structure, such as f(g(X),Y), and a list of the
variable bindings.

  The articles I ordered from our library have begun to trickle in.  I have
read the article you wrote in 1967 on renamable and semantic resolution, though
I haven't "digested" it, and the mini-tutorial about AGNESS from the IEEE in
1988.  I have the following articles on order which you wrote (or co-authored).

65   Experiments with a Deductive QA program
69   Completeness theorems for semantic resolution in consequence ...
79   Using rewrite rules for connection graphs to prove theorems

  The following articles are also on order.  I don't have the author's names
or the publications handy, but they are all from 1988 to present.  I expect
they will arrive early next week.

     A resolution rule for well formed formulae
     Unrestricted resolution versus N resolution
     An introduction to Knuth Bendix completion
     A restriction of factoring in binary resolution
     Many sorted inferences in automated theorem proving
     A comparison of the resolution calculus and the connection method...
     Replacing unification by constraint satisfaction to improve logic...
     Many hard examples for resolution
     A new reduction rule for the connection graph proof procedure
     Resolution theorem proving

  The article about replacing unification by constraint satisfaction is
interesting to me.  It claims to provide a more seamless integration
of procedural predicates and functions.  I ordered the papers about Knuth
Bendix completion and "sorted" inferences because these are topics I don't
know much about.

  I have been making progress on the theorem proving program using
a top-down approach.  I have a symbol table, a parser for wff's, and the
beginnings of the procedures to convert to conjuctive normal form.

  The symbol table is a flat array.  To insert a new symbol the table must
be searched to see if it is already stored.  This takes O(n) time.  The key
of a symbol is its index in the array, so to retrieve a symbol is very fast.

  The parser is recursive descent.  I used the following grammar, adapted from
Aho, Sethi, and Ullman's book.

   Start -> term5 $
   term5 -> term5 iff term4 | term4
   term4 -> term4 if term3 | term3
   term3 -> term3 or term2 | term2
   term2 -> term2 and term1 | term1
   term1 -> not term1
   term1 -> all atom term1
   term1 -> some atom term1
   term1 -> ( term5 )
   term1 -> term
   term  -> atom | atom() | atom(list)
   list  -> term, list | term

The "atom" can be either a variable, a constant symbol, or a number.  The
parser does permit expressions such as "all x (x(a) and 3(x))", but these
errors are detected later.

  I am following the algorithm in Genesereth and Nilsson's book to convert
to CNF.  I found an error in the algorithm in Rich's book:  it says to move
all quantifiers to the front of the expression before skolemizing, but one
needs to skolemize first.

  I speculated in the proposal that factoring can be applied to all clauses
as a simplification rule.  This is wrong as in the following example.

  1. f(X,a) or f(b,Y).
  2. -f(b,b).
  3. -f(a,a).

These three clauses are unsatisfiable.  But if I apply factoring to clause
(1) it becomes

  1'. f(b,a)

which is not inconsistent with (2) and (3).  Thus, not all clauses can be
replaced by their factored result.