Progress Report for Independent Study                      Nov 21, 1991

Dr. Slagle,

This week I worked out the problem of sharing variables.  Now all variables
within a clause are properly shared when the clause is created.  For example,
in f(x,x) both variables point to the same memory location, so when one
becomes bound, the other is also automatically.  I have just started
implementing unification, but I think that it will be very easy and efficient
since the variables are represented as pointers.

Another comment on the variables.  A "bound" variable points to an instance
of a term.  A "free" variable points to a special record denoting that it is
unbound.  Other free variables can also point to this record.  When a variable
is bound or shared during unification, the variable itself is not changed.
instead, the record it points to is changed.  If a variable is shared several
times before it is bound, it will point to a "chain" of records.

I notice something that suprized me at first.  The "exists" quantifier
is distributive over disjunction.  This means some x(f(x) or g(x)) is
equivalent to (some x f(x) or some y g(y)).  After skolemization we get
f($1) or g($1) is equivalent to f($2) or g($3).  At first it seemed to me
that the first is more restrictive, because the f-thing and g-thing have to
be the same.  After working out some examples, I can see why it doesn't
matter.

I see a problem with CGPP.  Before starting the proof, the graph has
many clauses and links representing information that the user has entered.
During the proof, links are removed and clauses with resulting purities
are also removed.  If the proof is successful, it is not unlikely that
the entire graph has been deleted.  This is not desirable.  It would be
better to retain the original clauses and links, but mark them as PRUNED.
They can be unmarked and used again in subsequent proofs.  It would also
be desirable to retain the clauses that were generated during the proof that
contributed to the refutation.  These are needed to display the "proof"
or explanation of the answer.  I don't know how to do this yet.

I am not very comfortable with how far along I am on the project.  I would
like to have the basic theorem prover done by now so that I can spend the
rest of the time doing extensions such as procedural predicates.  I don't
think my time was wasted, however.  There are many things that I understand
better now about quantifier scope and unification.  I will have to have
something done by next week so that I can work on the project report first
draft.

Sorry this report is so long.

John Henckel