Decision procedures are increasingly being employed for deciding or simplifying propositional combinations of ground equalities involving uninterpreted function symbols, linear arithmetic, arrays and other theories. Two approaches for constructing decision procedures for combination of ground theories were pioneered in the late seventies. In the approach of Nelson and Oppen, decision procedures for two disjoint theories are combined by introducing variables to name subterms and iteratively propagating any deduced equalities between variables from one theory to another. Shostak employs a different approach that works more efficiently in practice. He uses an optimized implementation of congruence closure procedure for ground equality over uninterpreted function symbols to combine theories that are canonizable and algebraically solvable. Many useful theories have these properties. Shostak's algorithm is subtle and complex and his description of this procedure is lacking rigor. We present, for the first time, a careful development and clarification of Shostak's procedure that corrects several mistakes in Shostak's original presentation. Our analysis serves as a useful basis for the implementation, extension, and further optimization of Shostak's decision procedure.

• cade96.pdf
• cade96.ps