Given a theory T and two formulas A and B jointly unsatisfiable in T, a _theory_
_interpolant_ of A and B is a formula I such that (i) its non-theory symbols are
shared by A and B, (ii) it is entailed by A in T, and (iii) it is unsatisfiable
with B in T. The practical importance of theory interpolants shows in model
checking, where they are used to accelerate the computation of reachability
relations. We present a novel method for computing ground interpolants for
ground formulas in the theory of equality. The method computes interpolants
from colored congruence graphs representing derivations in the theory of
equality. These graphs can be produced by conventional congruence closure
algorithms in a straightforward manner. By working with graphs, rather than at
the level of individual proof steps, we are able to derive interpolants that are
pleasingly simple (conjunctions of Horn clauses) and smaller than those produced
by the previous best algorithm. We demonstrate the advantages of our approach
with small illustrative examples and on a set of benchmarks derived from the
SMT-LIB suite.