Combining theories: the Ackerman and Guarded Fragments

Carlos Areces 1, 2 Pascal Fontaine 3, 4
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 - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
Cesare Tinelli and Viorica Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Oct 2011, Saarbrücken, Germany. Springer Verlag, 6989, pp.40--54, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24364-6_4〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00642529
Contributeur : Pascal Fontaine <>
Soumis le : vendredi 18 novembre 2011 - 11:26:58
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Lien texte intégral

Identifiants

Collections

Citation

Carlos Areces, Pascal Fontaine. Combining theories: the Ackerman and Guarded Fragments. Cesare Tinelli and Viorica Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Oct 2011, Saarbrücken, Germany. Springer Verlag, 6989, pp.40--54, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24364-6_4〉. 〈hal-00642529〉

Partager

Métriques

Consultations de la notice

200