Combining theories: the Ackerman and Guarded Fragments

Carlos Areces 1, 2 Pascal Fontaine 3
1 TALARIS - Natural Language Processing: representation, inference and semantics
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
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 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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-00642529
Contributor : Pascal Fontaine <>
Submitted on : Friday, November 18, 2011 - 11:26:58 AM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM

Links full text

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

229