The join of two sets of facts, E
1 and E
2, is defined as the set of all facts that are implied independently by both E
1 and E
2. Congruence closure is a widely used representation for sets of equational facts in the theory of uninterpreted function
symbols (UFS). We present an optimal join algorithm for special classes of the theory of UFS using the abstract congruence
closure framework. Several known join algorithms, which work on a strict subclass, can be cast as specific instantiations
of our generic procedure. We demonstrate the limitations of any approach for computing joins that is based on the use of congruence
closure. We also mention some interesting open problems in this area.
Research of the first and third authors was supported in part by NSF grants CCR-0081588, CCR-0085949, and CCR-0326577, and
gifts from Microsoft Research. Research of the second author was supported in part by NSF grant CCR-0326540 and NASA Contract
NAS1-20334.