A labelled sequent calculus for BBI: proof theory and proof search

DOI10.1093/LOGCOM/EXV033zbMATH Open1444.03159arXiv1302.4783OpenAlexW2591349272MaRDI QIDQ4612426

Publication date: 31 January 2019

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1302.4783

zbMATH Keywords

BBI automated reasoning proof theory labelled sequent calculus free variables

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: A labelled sequent calculus for BBI: proof theory and proof search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4612426)