The Undecidability of Boolean BI through Phase Semantics

Dominique Larchey-Wendling; Didier Galmiche

hal-00577919, version 1

The Undecidability of Boolean BI through Phase Semantics

Dominique Larchey-Wendling ¹, Didier Galmiche ¹

25th Annual IEEE Symposium on Logic in Computer Science - LICS 2010 (2010) 140-149

Résumé : We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the core of separation and spatial logics. For this, we define a complete phase semantics for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out a fragment of ILL which is both undecidable and complete for trivial phase semantics. Therefore, we obtain the undecidability of BBI.

1 : TYPES (LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

hal-00577919, version 1
http://hal.archives-ouvertes.fr/hal-00577919
oai:hal.archives-ouvertes.fr:hal-00577919
Contributeur : Dominique Larchey-Wendling <>
Soumis le : Jeudi 17 Mars 2011, 17:17:24
Dernière modification le : Lundi 28 Mars 2011, 12:22:55

Voir la fiche détaillée

Documents associés

PDF :

DOI : 10.1109/LICS.2010.18

Exporter

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>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="hal-00577919"><analytic>
<author><persName><forename>Dominique</forename><surname>Larchey-Wendling</surname></persName>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">TYPES</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>
<author><persName><forename>Didier</forename><surname>Galmiche</surname></persName>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">TYPES</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">The Undecidability of Boolean BI through Phase Semantics</title></analytic><monogr><title level="m" type="main">Proceedings of</title><meeting>25th Annual IEEE Symposium on Logic in Computer Science - LICS 2010</meeting><title level="j" type="main">Logic in Computer Science, Symposium on</title><imprint><publisher>IEEE</publisher><pubPlace><settlement>Edinburgh</settlement><country>Royaume-Uni</country></pubPlace><biblScope type="publicationDate">2010-00-00</biblScope><biblScope type="pp">140-149</biblScope></imprint></monogr><idno type="doi">10.1109/LICS.2010.18</idno><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00577919</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00577919/PDF/lics10_larchey_galmiche_full.pdf</idno></biblStruct>
</listBibl>
</listBibl>