Union-Find and Congruence Closure Algorithms that Produce Proofs
Robert Nieuwenhuis, Albert Oliveras · 2004
Congruence closure algorithms are nowadays central in many modern applications in automated deduction and verification, where it is frequently required to recover the set of merge operations that caused the equivalence of a given pair of terms. For this purpose we study, from the algorithmic point of view, the problem of extracting such small proofs.