### Join Algorithms for the Theory of Uninterpreted Functions

### Abstract

The join of two sets of facts, E1 and E2, is defined as the set of all
facts that are implied independently by both E1 and E2. 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.