Combining theories: the Ackerman and Guarded Fragments - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Combining theories: the Ackerman and Guarded Fragments

(1, 2) , (3)


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 a previous paper 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 (combinations of) theories, with only minor restrictions. In particular, it is not required for these other theories to be stably-infinite.

Dates and versions

hal-00642529 , version 1 (18-11-2011)



Carlos Areces, Pascal Fontaine. Combining theories: the Ackerman and Guarded Fragments. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Viorica Sofronie-Stokkermans, Oct 2011, Saarbrücken, Germany. pp.40--54, ⟨10.1007/978-3-642-24364-6_4⟩. ⟨hal-00642529⟩
112 View
0 Download



Gmail Facebook Twitter LinkedIn More