Sciweavers

CADE
2012
Springer

Combination of Disjoint Theories: Beyond Decidability

12 years 2 months ago
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.
Pascal Fontaine, Stephan Merz, Christoph Weidenbac
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where CADE
Authors Pascal Fontaine, Stephan Merz, Christoph Weidenbach
Comments (0)