A labelled sequent calculus for BBI: proof theory and proof search. (9th June 2015)

• Record Type: Journal Article
• Authors: Hóu, Zhé; Goré, Rajeev; Tiu, Alwen
• Is Part Of: Journal of logic and computation. Volume 28:Number 4(2018)
• Page Start: 809
• Page End: 872
• Publication Date: 2015-06-09
• Subjects: Labelled sequent calculus -- automated reasoning -- BBI -- free variables -- proof theory; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exv033
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: 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.