Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

DOI10.1017/S0960129509007567zbMath1169.03024MaRDI QIDQ3636908

Didier Galmiche, Dominique Larchey-Wendling

Publication date: 30 June 2009

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

Kripke semanticsseparation logiclogic of bunched implicationsspatial logictableau proof system

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (6)

Bringing Order to the Separation Logic Jungle ⋮ 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 ⋮ Bunched logics displayed ⋮ An algebraic glimpse at bunched implications and separation logic

Cites Work

• A calculus and logic of resources and processes
• Intuitionistic propositional logic is polynomial-space complete
• Elimination of quantifiers and undecidability in spatial logics for concurrency
• Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic
• Context logic as modal logic
• Deciding validity in a spatial logic for trees
• The semantics of BI and resource tableaux
• On the Almighty Wand
• Semantic Labelled Tableaux for Propositional BI
• Anytime, anywhere
• BI as an assertion language for mutable data structures
• Models and Separation Logics for Resource Trees

This page was built for publication: Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding