J.-C. Filliātre, S. Owre, H. Rueß, and N. Shankar. Deciding propositional combinations of equalities and inequalities. Unpublished, October 2001.

We address the problem of combining individual decision procedures into a single decision procedure. Our combination approach is based on using the canonizer obtained from Shostak's combination algorithm for equality. We illustrate our approach with a combination algorithm for equality, disequality, arithmetic inequality, and propositional logic. Unlike the Nelson-Oppen combination where the processing of equalities is distributed across different closed decision procedures, our combination involves the centralized processing of equalities in a single procedure. The termination argument for the combination is based on that for Shostak's algorithm. We also give soundness and completeness arguments.

[ bib | .ps ]

Back