 |
 |
|
|
| HAL: hal-00577919, version 1 |
| DOI: 10.1109/LICS.2010.18 |
| Detailed view |  Export this paper |
 |
| 25th Annual IEEE Symposium on Logic in Computer Science - LICS 2010, Edinburgh : United Kingdom (2010) |
|
|
|
|
| The Undecidability of Boolean BI through Phase Semantics |
|
|
| Dominique Larchey-Wendling 1Didier Galmiche 1 |
|
|
| (2010) |
|
|
|
| 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) |
|
|
|
|
|
|
|
|
|
| Subject | : | Computer Science/Logic in Computer Science Mathematics/Logic |
|
|
| Attached file list to this document: | |||||
|
|||||
|
|
|
| hal-00577919, version 1 | |
| http://hal.archives-ouvertes.fr/hal-00577919 | |
| oai:hal.archives-ouvertes.fr:hal-00577919 | |
| From: Dominique Larchey-Wendling | |
| Submitted on: Thursday, 17 March 2011 17:17:24 | |
| Updated on: Monday, 28 March 2011 12:22:55 | |
