Construction of Equality Graphs

Abstract

The theoretical and practical problems of equality reasoning in Automated Deduction are notorious. A new method is presented to cope with the enormous search space that usually arises when equational axioms are present. Starting from an empty graph a production system constructs graphs which represent solutions for simpler problems defined by abstraction. These graphs contain global information and are plans for guiding the search for a proof of the original problem, represented in the final graph. The construction of equality graphs is based on the idea to search for the differences between two terms by seperating toplevel symbol and subterms of a functional term. The impact of the explicit representation of information contained in the inference system on the control of inferences is discussed. Finally the method is compared to other equality reasoning methods.