Nondeterministic Phase Semantics and the Undecidability of Boolean BI

作者：Larchey Wendling Dominique^*; Galmiche Didier

来源：ACM Transactions on Computational Logic, 2013, 14(1): 6.

DOI：10.1145/2422085.2422091

• Theory
• Linear logic
• Boolean BI
• Minsky machines encoding
• decidability

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.

• 出版日期2013-2