Combining Theories: The Ackerman and Guarded Fragments

C. Areces and P. Fontaine. Combining Theories: The Ackerman and Guarded Fragments. In C. Tinelli and V. Sofronie-Stokkermans, editors, Proceedings of Frontiers of Combining Systems, 8th International Symposium, (FroCoS 2011), Lecture Notes in Computer Science, pp. 40–54, Springer, Saarbruecken, Germany, 2011.

Download

[pdf] 

Abstract

Combination of decision procedures is at the heart of Satisfiability Modulo Theories (SMT) solvers. It provides ways to compose decision procedures for expressive languages which mix symbols from various decidable theories. Typical combinations include (linear) arithmetic, uninterpreted symbols, arrays operators, etc. In [7] we showed that any first-order theory from the Bernays-Schonfinkel-Ramsey fragment, the two variable fragment, or the monadic fragment can be combined with virtually any other decidable theory. Here, we complete the picture by considering the Ackermann fragment, and several guarded fragments. All theories in these fragments can be combined with other decidable (combinations of) theories, with only minor restrictions. In particular, it is not required for these other theories to be stably-infinite.

BibTeX

@InCollection{Areces2011d,
  author =       "C. Areces and P. Fontaine",
  booktitle =    "Proceedings of Frontiers of Combining Systems, 8th
                 International Symposium, (FroCoS 2011)",
  publisher =    "Springer",
  title =        "Combining Theories: The {A}ckerman and Guarded
                 Fragments",
  year =         "2011",
  address =      "Saarbruecken, Germany",
  editor =       "C. Tinelli and V. Sofronie-Stokkermans",
  pages =        "40--54",
  series =       "Lecture Notes in Computer Science",
  volume =       "6989",
  abstract =     "Combination of decision procedures is at the heart of
                 Satisfiability Modulo Theories (SMT) solvers. It
                 provides ways to compose decision procedures for
                 expressive languages which mix symbols from various
                 decidable theories. Typical combinations include
                 (linear) arithmetic, uninterpreted symbols, arrays
                 operators, etc. In [7] we showed that any first-order
                 theory from the Bernays-Schonfinkel-Ramsey fragment,
                 the two variable fragment, or the monadic fragment can
                 be combined with virtually any other decidable theory.
                 Here, we complete the picture by considering the
                 Ackermann fragment, and several guarded fragments. All
                 theories in these fragments can be combined with other
                 decidable (combinations of) theories, with only minor
                 restrictions. In particular, it is not required for
                 these other theories to be stably-infinite.",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
  ee =           "http://dx.doi.org/10.1007/978-3-642-24364-6_4",
  ISBN =         "978-3-642-24363-9",
}