Nondeterministic Phase Semantics and the Undecidability of Boolean BI

被引：12
作者：
Larchey-Wendling, Dominique [1 ]
Galmiche, Didier [2 ]
机构：
[1] CNRS, LORIA, F-75700 Paris, France
[2] Univ Henri Poincare, LORIA, Nancy, France
来源：
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC | 2013年 / 14卷 / 01期
关键词：
Theory; Linear logic; Boolean BI; Minsky machines encoding; decidability; LINEAR LOGIC; PROOF;
D O I：
10.1145/2422085.2422091
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页数：41
相关论文
共 26 条
  • [1] [Anonymous], 1985, MONOGRAPHS THEORETIC
  • [2] Bouajjani A, 1997, LECT NOTES COMPUT SC, V1243, P135
  • [3] A Unified Display Proof Theory for Bunched Logic
    Brotherston, James
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2010, 265 (0C) : 197 - 211
  • [4] Undecidability of propositional separation logic and its neighbours
    Brotherston, James
    Kanovich, Max
    [J]. 25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 130 - 139
  • [5] Classical BI (A Logic for Reasoning about Dualising Resources)
    Brotherston, James
    Calcagno, Cristiano
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (01) : 328 - 339
  • [6] Deciding validity in a spatial logic for trees
    Calcagno, C
    Cardelli, L
    Gordon, AD
    [J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2005, 15 : 543 - 572
  • [7] Local action and abstract separation logic
    Calcagno, Cristiano
    O'Hearn, Peter W.
    Yang, Hongseok
    [J]. 22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, : 366 - +
  • [8] Vector addition tree automata
    de Groote, P
    Guillaume, B
    Salvati, S
    [J]. 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 64 - 73
  • [9] The semantics of BI and resource tableaux
    Galmiche, D
    Méry, D
    Pym, D
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2005, 15 (06) : 1033 - 1088
  • [10] Galmiche D, 2006, LECT NOTES COMPUT SC, V4337, P357
123