Combining theories: The Ackerman and Guarded fragments

Abstract. Combination of decision procedures is at the heart of Sat-isfiability Modulo Theories (SMT) solvers. It provides ways to compose decision procedures for expressive languages which mix symbols from var-ious decidable theories. Typical combinations include (linear) arithmetic, uninterpreted symbols, arrays operators, etc. In [7] we showed that any first-order theory from the Bernays-Schönfinkel-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 (com-binations of) theories, with only minor restrictions. In particular, it is not required for these other theories to be stably-infinite.