Combination of disjoint theories: beyond decidability

Pascal Fontaine, Stephan Merz, and Christoph Weidenbach

Abstract

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 refutationally complete 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.

© Springer-Verlag 2012

Available as: PDF

Reference

@InProceedings{fontaine:combination-beyond,
  author =       {Pascal Fontaine and Stephan Merz and Christoph Weidenbach},
  title =        {Combination of disjoint theories: beyond decidability},
  booktitle = {6th Intl. Joint Conf. Automated Reasoning (IJCAR 2012)},
  pages =     {256-270},
  year =      2012,
  editor =    {Bernhard Gramlich and Dale Miller and Uli Sattler},
  volume =    {7364},
  series =    {LNCS},
  address =   {Manchester, UK},
  publisher = {Springer},
}