The Undecidability of Boolean BI through Phase Semantics

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.

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Dominique Larchey-Wendling, Didier Galmiche
• Keywords: Automated Reasoning, Complete Phase Semantics, LICS 2010, Logic, Trivial Phase Semantics