Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/142650
Title: A labelled sequent calculus for BBI : proof theory and proof search
Authors: Hóu, Zhé
Goré, Rajeev
Tiu, Alwen
Keywords: Engineering::Computer science and engineering
Issue Date: 2015
Source: Hóu, Z., Goré, R., & Tiu, A. (2018). A labelled sequent calculus for BBI : proof theory and proof search. Journal of Logic and Computation, 28(4), 809-872. doi:10.1093/logcom/exv033
Journal: Journal of Logic and Computation
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.
URI: https://hdl.handle.net/10356/142650
ISSN: 0955-792X
DOI: 10.1093/logcom/exv033
Rights: © 2015 The Author(s). All rights reserved. This paper was published by Oxford University Press in Journal of Logic and Computation and is made available with permission of The Author(s).
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Journal Articles

Files in This Item:
File Description SizeFormat 
A labelled sequent calculus for BBI - Proof theory and proof search.pdf468.68 kBAdobe PDFView/Open

Page view(s) 50

12
checked on Sep 30, 2020

Download(s) 50

4
checked on Sep 30, 2020

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.