Hou, ZheTiu, AlwenGore, RajeevGalmiche, D.Larchey-Wendling, D.2015-12-10September9783642405365http://hdl.handle.net/1885/65771We present a labelled sequent calculus for Boolean BI (BBI), a classical variant of the logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e., those rKeywords: Bunched implications; Concrete model; Constraint systems; Cut elimination; Logical rules; Sequent calculus; Structural rules; Ternary relations; Differentiation (calculus); Heuristic methods; Semantics; Calculations201310.1007/978-3-642-40537-2_162019-08-11