# A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

arXiv: https://arxiv.org/abs/1302.4783 · HTML: https://mlsanity.com/paper/1302.4783/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Feb 2013.

## Built on by (most cited first, 1 of 1)

- [Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification](https://mlsanity.com/paper/2503.22755/) (2025)

## Abstract (arXiv)

We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in our proof system, including those rules that manipulate labels, can be localised around applications of certain logical rules, thereby localising the handling of these rules in proof search. Based on this, we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. A heuristic method to solve the constraints is proposed in the end, with some experimental results.