A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses

. We present Dedam (Deduction Abstact Machine), a standard architecture around which high-performance theorem provers for clausal logic with equality can be built. It includes a WAM-like heap structure for storing terms as DAG's, several indexing data structures, and mechanisms for efficient memory management and demodulation. These data structures turn out to be surprisingly well combinable due to conceptual similarities. We provide statistics showing how we reduce two well-known bottlenecks in equational deduction. The first one, matching for demodulation is done by a new indexing method, substitution trees with equality constraints. Regarding the other bottle neck, memory management, WAM-based techniques allow us to completely avoid it during unification, matching, and demodulation. Static clause (sub)sets can be compiled in this framework into efficient abstract machine code for inference computation and redundancy proving. 1 Introduction During the last decade, research on automa..