Combinations of theories for decidable fragments of first-order logic
Identifieur interne : 001558 ( Hal/Curation ); précédent : 001557; suivant : 001559Combinations of theories for decidable fragments of first-order logic
Auteurs : Pascal Fontaine [France]Source :
Abstract
The design of decision procedures for first-order theories and their combinations has been a very active research subject for thirty years; it has gained practical importance through the development of SMT (satisfiability modulo theories) solvers. Most results concentrate on combining decision procedures for data structures such as theories for arrays, bitvectors, fragments of arithmetic, and uninterpreted functions. In particular, the well-known Nelson-Oppen scheme for the combination of decision procedures requires the signatures to be disjoint and each theory to be stably infinite; every satisfiable set of literals in a stably infinite theory has an infinite model. In this paper we consider some of the best-known decidable fragments of first-order logic with equality, including the Löwenheim class (monadic FOL with equality, but without functions), Bernays-Schönfinkel-Ramsey theories (finite sets of formulas of the form $\exists^*\forall^* \varphi$, where $\varphi$ is a function-free and quantifier-free FOL formula), and the two-variable fragment of FOL. In general, these are not stably infinite, and the Nelson-Oppen scheme cannot be used to integrate them into SMT solvers. Noticing some elementary results about the cardinalities of the models of these theories, we show that they can nevertheless be combined with almost any other decidable theory.
Url:
DOI: 10.1007/978-3-642-04222-5_16
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001558
Links to Exploration step
Hal:inria-00430631Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Combinations of theories for decidable fragments of first-order logic</title><author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2357" status="OLD"><idno type="RNSR">200418303G</idno><orgName>Proof-oriented development of computer-based systems</orgName><orgName type="acronym">MOSEL</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/mosel</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00430631</idno><idno type="halId">inria-00430631</idno><idno type="halUri">https://hal.inria.fr/inria-00430631</idno><idno type="url">https://hal.inria.fr/inria-00430631</idno><idno type="doi">10.1007/978-3-642-04222-5_16</idno><date when="2009-09-16">2009-09-16</date><idno type="wicri:Area/Hal/Corpus">001558</idno><idno type="wicri:Area/Hal/Curation">001558</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Combinations of theories for decidable fragments of first-order logic</title><author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2357" status="OLD"><idno type="RNSR">200418303G</idno><orgName>Proof-oriented development of computer-based systems</orgName><orgName type="acronym">MOSEL</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/mosel</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></analytic><idno type="DOI">10.1007/978-3-642-04222-5_16</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The design of decision procedures for first-order theories and their combinations has been a very active research subject for thirty years; it has gained practical importance through the development of SMT (satisfiability modulo theories) solvers. Most results concentrate on combining decision procedures for data structures such as theories for arrays, bitvectors, fragments of arithmetic, and uninterpreted functions. In particular, the well-known Nelson-Oppen scheme for the combination of decision procedures requires the signatures to be disjoint and each theory to be stably infinite; every satisfiable set of literals in a stably infinite theory has an infinite model. In this paper we consider some of the best-known decidable fragments of first-order logic with equality, including the Löwenheim class (monadic FOL with equality, but without functions), Bernays-Schönfinkel-Ramsey theories (finite sets of formulas of the form $\exists^*\forall^* \varphi$, where $\varphi$ is a function-free and quantifier-free FOL formula), and the two-variable fragment of FOL. In general, these are not stably infinite, and the Nelson-Oppen scheme cannot be used to integrate them into SMT solvers. Noticing some elementary results about the cardinalities of the models of these theories, we show that they can nevertheless be combined with almost any other decidable theory.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Combinations of theories for decidable fragments of first-order logic</title><author role="aut"><persName><forename type="first">Pascal</forename><surname>Fontaine</surname></persName><email>Pascal.Fontaine@loria.fr</email><idno type="idhal">pascal-fontaine</idno><idno type="halauthor">63592</idno><affiliation ref="#struct-2357"></affiliation></author><editor role="depositor"><persName><forename>Pascal</forename><surname>Fontaine</surname></persName><email>Pascal.Fontaine@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2009-11-09 12:33:38</date><date type="whenModified">2016-05-19 01:09:17</date><date type="whenReleased">2009-11-09 12:33:38</date><date type="whenProduced">2009-09-16</date></edition><respStmt><resp>contributor</resp><name key="103615"><persName><forename>Pascal</forename><surname>Fontaine</surname></persName><email>Pascal.Fontaine@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00430631</idno><idno type="halUri">https://hal.inria.fr/inria-00430631</idno><idno type="halBibtex">fontaine:inria-00430631</idno><idno type="halRefHtml">Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium, FroCoS 2009, Sep 2009, Trento, Italy. Springer Verlag, 5749, pp.263-278, 2009, Lecture Notes in Computer Science; Frontiers of Combining Systems. <10.1007/978-3-642-04222-5_16></idno><idno type="halRef">Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium, FroCoS 2009, Sep 2009, Trento, Italy. Springer Verlag, 5749, pp.263-278, 2009, Lecture Notes in Computer Science; Frontiers of Combining Systems. <10.1007/978-3-642-04222-5_16></idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno></seriesStmt><notesStmt><note type="commentary">The original publication is available at www.springerlink.com</note><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Combinations of theories for decidable fragments of first-order logic</title><author role="aut"><persName><forename type="first">Pascal</forename><surname>Fontaine</surname></persName><email>Pascal.Fontaine@loria.fr</email><idno type="idHal">pascal-fontaine</idno><idno type="halAuthorId">63592</idno><affiliation ref="#struct-2357"></affiliation></author></analytic><monogr><meeting><title>7th International Symposium, FroCoS 2009</title><date type="start">2009-09-16</date><date type="end">2009-09-18</date><settlement>Trento</settlement><country key="IT">Italy</country></meeting><editor>Silvio Ghilardi and Roberto Sebastiani</editor><imprint><publisher>Springer Verlag</publisher><biblScope unit="serie"></biblScope><biblScope unit="volume">5749</biblScope><biblScope unit="pp">263-278</biblScope><date type="datePub">2009</date></imprint></monogr><idno type="doi">10.1007/978-3-642-04222-5_16</idno></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><abstract xml:lang="en">The design of decision procedures for first-order theories and their combinations has been a very active research subject for thirty years; it has gained practical importance through the development of SMT (satisfiability modulo theories) solvers. Most results concentrate on combining decision procedures for data structures such as theories for arrays, bitvectors, fragments of arithmetic, and uninterpreted functions. In particular, the well-known Nelson-Oppen scheme for the combination of decision procedures requires the signatures to be disjoint and each theory to be stably infinite; every satisfiable set of literals in a stably infinite theory has an infinite model. In this paper we consider some of the best-known decidable fragments of first-order logic with equality, including the Löwenheim class (monadic FOL with equality, but without functions), Bernays-Schönfinkel-Ramsey theories (finite sets of formulas of the form $\exists^*\forall^* \varphi$, where $\varphi$ is a function-free and quantifier-free FOL formula), and the two-variable fragment of FOL. In general, these are not stably infinite, and the Nelson-Oppen scheme cannot be used to integrate them into SMT solvers. Noticing some elementary results about the cardinalities of the models of these theories, we show that they can nevertheless be combined with almost any other decidable theory.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001558 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 001558 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Curation
|type= RBID
|clé= Hal:inria-00430631
|texte= Combinations of theories for decidable fragments of first-order logic
}}
| This area was generated with Dilib version V0.6.33. |  |