An Implementation Kernel for Theorem Proving with Equality Clauses

We provide a standard abstract architecture around which high-performance theorem provers for full clausal logic with equality can be built. A WAM-like heap structure for storing terms (as DAG's, with structure sharing) and several substitution trees [Gra95b] are central in the architecture. These two data structures turn out to be surprisingly well combinable due to conceptual similarities. Indexing techniques based on substitution trees outperform previous methods, and are integrated in such a way that e.g. no writing on the heap is needed during (many-to-one) term unification. Static clause (sub)sets can be compiled in this framework into efficient abstract machine code for inference computation and redundancy proving. Finally, as an example, a toy equational completion system based on the framework is described. This work has been partially supported by the European Esprit Working Group CCL, ref. 6028 and the European HCM network ConSolE. 1 Introduction The equality predicate..