Progress Report for Independent Study                 Nov. 12, 1991

Dr. Slagle,

This week I wrote the heap management functions.  In the last note I said
I would use a pointers to connect the heap.  Soon after, I realized an array
is more efficient.

I have implemented procedures to create new clauses.  This has a problem,
however, that variables within a clause are not shared properly.
I have written procedures to delete a clause.  This also deletes all links
refering to the clause. When a link is deleted, the clauses it refers to are
updated and may also be deleted if they have purities.

I am calling a collection of clauses with links between them a graph.
The top level functions will operate on graphs.  The proof procedure will,
given a graph, try to derive the empty clause.  The "merge" procedure will,
given two graphs, merge the first into the second.

I need to write unification functions which create new links.


John Henckel