Nondeterministic Phase Semantics and the Undecidability of Boolean BI
Dominique Larchey-Wendling, Didier Galmiche · ACM Transactions on Computational Logic · 2013
We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered the core of separation and spatial logics. For this, we define a complete phase semantics suitable 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 the elementary fragment of ILL, which is both undecidable and complete for trivial phase semantics. Thus, we obtain the undecidability of BBI.