Combining theories: the Ackerman and Guarded Fragments

Carlos Areces; Pascal Fontaine

hal-00642529, version 1

Combining theories: the Ackerman and Guarded Fragments

Carlos Areces ()^a^, 1, 2, Pascal Fontaine (, ) ^3, 4

8th International Symposium Frontiers of Combining Systems - FroCoS 2011 6989 (2011) 40--54

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.

a – INRIA
1: TALARIS (INRIA Nancy - Grand Est / LORIA)
CNRS : UMR7503 – INRIA – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2: Facultad de Matemática, Astronomía y Física [Cordoba] (FaMAF)
Universidad Nacional de Córdoba
3: VERIDIS (INRIA Nancy - Grand Est / LORIA)
Université de Lorraine – CNRS : UMR7503 – INRIA
4: MOSEL (LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

hal-00642529, version 1
http://hal.inria.fr/hal-00642529
oai:hal.inria.fr:hal-00642529
From: Pascal Fontaine <>
Submitted on: Friday, 18 November 2011 11:26:58
Updated on: Wednesday, 23 November 2011 15:12:47

See detailed view

Associated documents

DOI: 10.1007/978-3-642-24364-6_4

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00642529"><analytic>
<author><persName><forename>Carlos</forename><surname>Areces</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Nancy - Grand Est / LORIA</orgName>
<orgName type="team">TALARIS</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">FaMAF</orgName>
<orgName type="team">Facultad de Matemática, Astronomía y Física [Cordoba]</orgName>
<country>AR</country>
<orgName type="institution">Universidad Nacional de Córdoba</orgName>
</affiliation>
</author>
<author><persName><forename>Pascal</forename><surname>Fontaine</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Nancy - Grand Est / LORIA</orgName>
<orgName type="team">VERIDIS</orgName>
<country>FR</country>
<orgName type="institution">Université de Lorraine</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">INRIA</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">Combining theories: the Ackerman and Guarded Fragments</title></analytic><monogr><meeting>8th International Symposium Frontiers of Combining Systems - FroCoS 2011</meeting><imprint><publisher>Springer Verlag</publisher><pubPlace><settlement>Saarbrücken</settlement><country>Germany</country></pubPlace><biblScope type="publicationDate">2011-00-00</biblScope><biblScope type="vol">6989</biblScope><biblScope type="pp">40--54</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-24364-6_4</idno><idno type="HALid">http://hal.inria.fr/hal-00642529</idno></biblStruct>
</listBibl>
</listBibl>