Progress Report for Independent Study                 Nov. 6, 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.


  When measured by lines-of-code, I have not made much progress this week.
I have been wrestling with the data structures (and algorithms) to use
for representing sets of clauses and the "links" in the connection graph.

  Each clause has at least one literal.  Each literal has a "structure", (a
tree of a predicate, functions, constants, and variables), a list of variable
bindings, and a list of the links which point to it.  Each link points
to two literals, (the clause containing each literal is also indicated).  The
two types of links are resolution and factoring.  Each link has a variable
assignment list.  This is a list indicating how to bind the variables in the
two clauses when the action indicated by the type of the link is performed.
Each link has a score.  The reasoning procedure always performs the link with
the highest score first.

  I am implementing this as follows.  The clauses are stored in a doubly-linked
list.  The literals for each clause are stored in an array.  The list of
variables' bindings for each literal is stored in an array.  I need to store
the links in a data structure that allows efficient delete-max, delete-any,
and insert.  This kind of structure is called a priority queue, and it can
be easily implemented with a heap.  Since a heap is a complete binary tree,
it is usually implemented as an array.  The binary tree is rearranged by
moving the elements of the array.  This will not work in my program because
the links are pointed to by the literals, so the links cannot be moved
around in memory.