Abstract

We are improving equality reasoning in automatic theorem-provers, and congruence classes provide an efficient storage mechanism for terms, as well as the congruence closure decision procedure. We describe the technical steps involved in integrating logic variables with congruence classes, and present an algorithm that can be proved to find all matches between classes . An application of this algorithm makes possible a percolation algorithm for undirected rewriting in minimal space; this is described and an implementation in hol98 is examined in some detail