TY - JOUR
T1 - A labelled sequent calculus for BBI
T2 - Proof theory and proof search
AU - Hóu, Zhé
AU - Goré, Rajeev
AU - Tiu, Alwen
N1 - Publisher Copyright:
© 2015 The Author.
PY - 2018/6/7
Y1 - 2018/6/7
N2 - We present a labelled sequent calculus for Boolean bunched implications (BBI), a classical variant of the logic of Bunched Implications (BI). The calculus is simple, sound, complete and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e. those rules that manipulate labels and ternary relations, can be localized around applications of certain logical rules, thereby localizing 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. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Additionally, we show that different semantics for BBI and some axioms in concrete models can be captured modularly simply by adding extra structural rules.
AB - We present a labelled sequent calculus for Boolean bunched implications (BBI), a classical variant of the logic of Bunched Implications (BI). The calculus is simple, sound, complete and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e. those rules that manipulate labels and ternary relations, can be localized around applications of certain logical rules, thereby localizing 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. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Additionally, we show that different semantics for BBI and some axioms in concrete models can be captured modularly simply by adding extra structural rules.
KW - BBI
KW - Labelled sequent calculus
KW - automated reasoning
KW - free variables
KW - proof theory
UR - http://www.scopus.com/inward/record.url?scp=85061707298&partnerID=8YFLogxK
U2 - 10.1093/logcom/exv033
DO - 10.1093/logcom/exv033
M3 - Article
SN - 0955-792X
VL - 28
SP - 809
EP - 872
JO - Journal of Logic and Computation
JF - Journal of Logic and Computation
IS - 4
ER -