Proof search for propositional abstract separation logics via labelled sequents

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are “abstract ” because they are independent of any particular concrete memory model. Their assertion languages, called propositional ab-stract separation logics, extend the logic of (Boolean) Bunched Im-plications (BBI) in various ways. We develop a modular proof theory for various propositional abstract separation logics using cut-free labelled sequent calculi. We first extend the cut-fee labelled sequent calculus for BBI of Hóu et al to handle Calcagno et al’s original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We prove the completeness of our calculus via a sound intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other propositional abstract separation logics by adding sound rules for indivisible unit and disjointness, while maintaining completeness and cut-elimination. We present a theorem prover based on our labelled calculus for these logics