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 |
---|---|
其他作者: | School of Computer Science and Engineering |
格式: | Article |
語言: | English |
出版: |
2020
|
主題: | |
在線閱讀: | https://hdl.handle.net/10356/142650 |
標簽: |
添加標簽
沒有標簽, 成為第一個標記此記錄!
|
機構: | Nanyang Technological University |
語言: | English |
相似書籍
-
Extracting proofs from tabled proof search
由: Miller, Dale., et al.
出版: (2013) -
Truth in a Logic of Formal Inconsistency: How classical can it get?
由: LAVINIA MARIA PICOLLO
出版: (2021) -
Ophthalmic bottle labeling machine
由: Andaluz, Francis Gabriel, et al.
出版: (2009) -
Automated pressure-sensitive labeling machine
由: Carino, Faye Marie Goyena, et al.
出版: (2002) -
Computability via the lambda-calculus with patterns
由: Bodin Skulkiat
出版: (2012)