Nondeterministic phase semantics and the undecidability of Boolean BI

DOI10.1145/2422085.2422091MaRDI QIDQ2946690zbMATH OpenOpenAlexFDO

Authors Dominique Larchey-Wendling, Didier Galmiche

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2422085.2422091

zbMATH Keywords

Boolean BIdecidabilitylinear logicMinsky machines encoding

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05)

Recommendations

• On Model Checking Boolean BI
• Undecidability of propositional separation logic and its neighbours
• Expressivity Properties of Boolean BI Through Relational Models
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
• The semantics of BI and resource tableaux

Cited in

(18)

• Proof tactics for assertions in separation logic
• Separation logic with one quantified variable
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Exponential-size model property for PDL with separating parallel composition
• Two-Variable Separation Logic and Its Inner Circle
• A unified display proof theory for bunched logic
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
• Completeness for a first-order abstract separation logic
• Undecidability of propositional separation logic and its neighbours
• On Model Checking Boolean BI
• On the almighty wand
• Separation logics and modalities: a survey
• scientific article; zbMATH DE number 7204446 (Why is no real title available?)
• A complete axiomatisation for quantifier-free separation logic
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressivity Properties of Boolean BI Through Relational Models
• An epistemic separation logic with action models
• An algebraic glimpse at bunched implications and separation logic

This page was built for publication: Nondeterministic phase semantics and the undecidability of Boolean BI

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946690)