@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",
}