Semantic labelled tableaux for propositional BI
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 BIperpendicular to1 based on particular labels and constraints. We prove the soundness and completeness of this calculus w.r.t. the Kripke resource semantics with emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability of BIperpendicular to. Moreover, we analyse 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.
semantics intuitionistic logic tableau method bi logic labelled deduction