Proof-producing congruence closure

Abstract

Many applications of congruence closure nowadays require the ability of recovering, among the thousands of input equations, the small subset that caused the equivalence of a given pair of terms. For this purpose, here we introduce an incremental congruence closure algorithm that has an additional Explain operation. First, two variations of union-find data structures with Explain are introduced. Then, these are applied inside a congruence closure algorithm with Explain, where a κ-step proof can be recovered in almost optimal time (quasi-linear in κ), without increasing the overall O(n log n) runtime of the fastest known congruence closure algorithms. This non-trivial (ground) equational reasoning result has been quite intensively sought after (see, e.g., [SD99, dMRS04, KS04]), and moreover has important applications to verification. © Springer-Verlag Berlin Heidelberg 2005.