Towards a Cut-free Sequent Calculus for Boolean BI
Sungwoo Park, Jong‐Hyun Park · EPiC series in computing · 2018
The logic of bunched implications (BI) of O’Hearn and Pym [5] is a substructural logic which freely combines additive connectives ⊃, ∧, ∨ from propositional logic and multiplicative connectives −⋆, ⋆ from linear logic. Because of its concise yet rich representation of states of resources, BI is regarded as a logic suitable for reasoning about resources. For example, by building amodel forBIbasedonamonoidofheaps, weobtainseparationlogic[7]which extends Hoare logic to facilitate reasoning about imperative programs manipulating heap memory. Depending on its interpretation of additive connectives, BI comes with two flavors: intuitionistic BI and boolean BI. Intuitionistic BI interprets additive connectives intuitionistically, while boolean BI interprets additive connectives classically and admits such principles as the law of excluded middle. Both logics interpret multiplicative connectives intuitionistically and do not introduce multiplicative falsity or negation. Intuitionistic BI has a well-developed proof theory. It has a natural deduction system with the normalization property and also a cut-free sequent calculus. Because free combinations of additive connectivesand multiplicative connectivesare allowed, contexts in such proof-theoretic formulations are not unordered sets as usual, but bunches: trees whose internal nodes indicate