A labelled sequent calculus for BBI : proof theory and proof search
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 la...
Saved in:
Main Authors: | Hóu, Zhé, Goré, Rajeev, Tiu, Alwen |
---|---|
Other Authors: | School of Computer Science and Engineering |
Format: | Article |
Language: | English |
Published: |
2020
|
Subjects: | |
Online Access: | https://hdl.handle.net/10356/142650 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Nanyang Technological University |
Language: | English |
Similar Items
-
Extracting proofs from tabled proof search
by: Miller, Dale., et al.
Published: (2013) -
Truth in a Logic of Formal Inconsistency: How classical can it get?
by: LAVINIA MARIA PICOLLO
Published: (2021) -
Computability via the lambda-calculus with patterns
by: Bodin Skulkiat
Published: (2012) -
Ophthalmic bottle labeling machine
by: Andaluz, Francis Gabriel, et al.
Published: (2009) -
Automated pressure-sensitive labeling machine
by: Carino, Faye Marie Goyena, et al.
Published: (2002)