Progress Report for Independent Study                 Oct. 29, 1991

Dr. Slagle,

  This week I finished the procedures to convert to CNF.  Next week I will
work on the unification procedures (used to create new links in the
connection graph) and the procedures to store the links in a heap.

  I read these papers this week:

65  Robinson, J.A., A Machine-Oriented Logic Based on the Resolution
    Principle, JACM, v12 n1, 1965, 23-41.

88  Chvatal, V., Szemeredi, E., Many Hard Examples for Resolution.  JACM, v35
    n4, 1988, 759-768.

86  Digricoli, V.J., M.C. Harrison, Equality-Based Binary Resolution, JACM,
    v33 n2, 1986, 253-289.

88  Stickel, M.E., Resolution Theorem Proving, Annual Review of Computer
    Science, v3, 1988, 285-316.

88  Munch, K.H., A New Reduction Rule for the Connection Graph Proof
    Procedure.  Journal of Automated Reasoning, v4, 1988, 425-444.

90  Roach, J.W., Sundararajan, R., Watson, L.T., Replacing Unification by
    Constraint Satisfaction to Improve Logic Program Expressiveness.  Journal
    of Automated Reasoning, v6, 1990, 51-75.

91  Hsiang, J., Rusinowitch, M., Proving Refutational Completeness of
    Theorem-Proving Strategies:  The Transfinite Semantic Tree Method.  JACM,
    v38 n3, 1991, 559-587.

  I had never read Robinson's landmark paper on resolution before.  I was
surprized at all the topics it covered: unification, resolution, purity,
subsumption, etc.

  The paper by Chvatal is not very readable or useful, I think.  It shows
that a randomly generated set of clauses in propositional logic is probably
unsatisfiable under certain constraints.

  I have been thinking quite a bit about equality.  One must read a variety
of papers to get a realistic view on the state of this topic.  The choices
for handling equality are:  using explicit axioms, rewrite rules,
paramodulation, or RUE.  These are the only choices I know of.

  The axiomization method is inefficient because the equality axioms are so
general they generate large numbers of resolvents, mostly redundant.
This method is logically complete.

  The rewrite rules method (demodulation) is used to convert clauses to
canonical form before they are retained.  This method reduces the amount
of redundant information.  Knuth-Bendix completion can expand the set of
rewrite rules so that they are terminating and confluent.  Converting every
clause to an irreducible normal form facilitates equality reasoning.
However, this method is not logically complete.

  Paramodulation seems to be the most popular method for reasoning with
equality.  It theory, resolution with paramodulation has been proven
logically complete.  However, the completeness requires that every permu-
tation of paramodulation and resolution is performed.  This would be
just as inefficient as axiomization.  Instead, most systems only apply
paramodulation to disagreements in unification.

  The RUE method (Digricoli 86) merges paramodulation and resolution into
a single inference rule.  During unification, a disagreement set is generated
which is attached to the resolvent.  It would be easier to implement a
logically complete version of this rule than paramodulation.  However,
it would not be more or less efficient.

  In conclusion, I think axiomization is the simplest to implement.  The
other methods do not offer significant advantages.  Also I prefer
axiomization because my impression is that it will be the easiest to
integrate with procedural functions and predicates.

  The article about constraint satisfaction by Roach was not what I expected.
It is an extension to the Prolog interpreter and it only supports linear
functions and inequalities, + - < >.

  I found the paper by Mark Stickel to be very informative and well written.
It gives a better introduction to theorem proving than any text book I've
seen.  He discusses Kowalski's connection graph method (CGPP).  In
the proposal I discussed how a link that is resolved on is removed from the
graph, and this prevents it from being used again even by a descendant
clause.  This prunes the search space similar to hyper-resolution.
This causes CGPP to be noncommutative (changes to the graph are irrevocable).
An example has been shown of an unsatisfiable set of clauses for which CGPP
cannot derive the empty clause because it reaches a dead end.  Backtracking
is required to restore the state of the graph.  Backtracking is too expensive
to be practical.  I wonder if there is a way to modify CGPP so that it is
confluent.

  The paper by Munch on the v-rule for CGPP is very good.  He formalized
CGPP and discusses rules for resolution, subsumption, factoring, tautology,
purity, and var values (the new rule).  I intend to implement as many of
these as I can in my project.  He also discusses the problem of
refutation confluence of CGPP.

  I have requested an IBM technical report by C.L Chang on DEDUCE.
I am curious to see how he decides when to do logic inferences and when
to query the relational database for facts.

  I think I had better do less reading now so I can finish the computer
program part of my project.