An improved algorithm for computing with equations

Implementation of programming language interpreters, proving theorems of the form A=B, and implementation of abstract data types are all problems that can be reduced to the problem of finding a normal form for an expression with respect to a finite set of equation (axiom) schemata The definition of a nonoverlapping s set of axiom schemata is given and the directed congruence closure algorithm is presented; an algorithm that efficiently solves this kind of problem provided the axiom schemata are nonoverlapping. The algorithm is a variation on the congruence closure algorithm? and, like the congruence closure algorithm, it has the advantage of remembering which expressions have already been proved to be equivalent. However, unlike the congruence closure algorithm, which can use only a finite set of axioms, the directed congruence closure algorithm allows a possibly infinite set of axioms generated by a finite set of axiom schemata.