Combination of Disjoint Theories: Beyond Decidability

Combination of theories underlies the design of satisfiability modulo theories (SMT) solvers. The Nelson-Oppen framework can be used to build a decision procedure for the combination of two disjoint decidable stably infinite theories. We here study combinations involving an arbitrary first-order theory. Decidability is lost, but refutational completeness is preserved. We consider two cases and provide complete (semi-)algorithms for them. First, we show that it is possible under minor technical conditions to combine a decidable (not necessarily stably infinite) theory and a disjoint finitely axiomatized theory, obtaining a refutationally complete procedure. Second, we provide a refutationally complete procedure for the union of two disjoint finitely axiomatized theories, that uses the assumed procedures for the underlying theories without modifying them.

• Type: Journal
• Year: 2012
• Where: CADE
• Authors: Pascal Fontaine, Stephan Merz, Christoph Weidenbach
• Keywords: CADE 2012, Decidability, Decision Procedure, Logical Reasoning, Study Combinations