HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Semantic Labelled Tableaux for propositional BI (without bottom)

Didier Galmiche 1 Daniel Méry 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we study semantic labelled tableaux for the propositional Bunched Implications logic (BI) that freely combines intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BI is a resource-aware logic that captures interferences between resources and it is well suited, because of its resource-based sharing interpretation, for reasoning about mutable data structures. We propose a labelled tableau calculus for BI without bottom, that is the unit of the additive disjunction, based on particular labels and constraints. We prove the soundness and completeness of this calculus wrt the Kripke resource semantics with an emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability. Moreover, we analyze some algorithmic aspects of the tableau construction by providing a free variable variant of the calculus. We also develop the restrictions to IL and MILL that provide new tableau methods for both logics with generation of countermodels.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:38:41 AM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM


  • HAL Id : inria-00099556, version 1



Didier Galmiche, Daniel Méry. Semantic Labelled Tableaux for propositional BI (without bottom). Journal of Logic and Computation, Oxford University Press (OUP), 2003, 13 (5), pp.707-753. ⟨inria-00099556⟩



Record views