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

TL;DR

This paper introduces a labelled sequent calculus for Boolean BI, enhancing proof search efficiency through localised structural rules and a lazy constraint-based approach, with experimental validation.

Contribution

It develops a simple, sound, complete calculus for Boolean BI with localised structural rules and a novel lazy constraint-based proof search method.

Findings

The calculus is sound and complete with cut-elimination.

Structural rules can be localised around logical rules.

Experimental results support the proposed heuristic method.

Abstract

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.