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
First, two variations of union-find data structures with
are introduced. Then, these are applied inside a congruence closure algorithm with
, where a
-step proof can be recovered in almost optimal time (quasi-linear in
), without increasing the overall
) 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.