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...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/142650 |
| _version_ | 1826124153360482304 |
|---|---|
| author | Hóu, Zhé Goré, Rajeev Tiu, Alwen |
| author2 | School of Computer Science and Engineering |
| author_facet | School of Computer Science and Engineering Hóu, Zhé Goré, Rajeev Tiu, Alwen |
| author_sort | Hóu, Zhé |
| collection | NTU |
| description | 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. |
| first_indexed | 2024-10-01T06:16:00Z |
| format | Journal Article |
| id | ntu-10356/142650 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T06:16:00Z |
| publishDate | 2020 |
| record_format | dspace |
| spelling | ntu-10356/1426502020-06-26T03:08:49Z A labelled sequent calculus for BBI : proof theory and proof search Hóu, Zhé Goré, Rajeev Tiu, Alwen School of Computer Science and Engineering Engineering::Computer science and engineering Labelled Sequent Calculus Automated Reasoning 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. Accepted version 2020-06-26T03:08:49Z 2020-06-26T03:08:49Z 2015 Journal Article 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 0955-792X https://hdl.handle.net/10356/142650 10.1093/logcom/exv033 2-s2.0-85061707298 4 28 809 872 en Journal of Logic and Computation © 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). application/pdf |
| spellingShingle | Engineering::Computer science and engineering Labelled Sequent Calculus Automated Reasoning Hóu, Zhé Goré, Rajeev Tiu, Alwen A labelled sequent calculus for BBI : proof theory and proof search |
| title | A labelled sequent calculus for BBI : proof theory and proof search |
| title_full | A labelled sequent calculus for BBI : proof theory and proof search |
| title_fullStr | A labelled sequent calculus for BBI : proof theory and proof search |
| title_full_unstemmed | A labelled sequent calculus for BBI : proof theory and proof search |
| title_short | A labelled sequent calculus for BBI : proof theory and proof search |
| title_sort | labelled sequent calculus for bbi proof theory and proof search |
| topic | Engineering::Computer science and engineering Labelled Sequent Calculus Automated Reasoning |
| url | https://hdl.handle.net/10356/142650 |
| work_keys_str_mv | AT houzhe alabelledsequentcalculusforbbiprooftheoryandproofsearch AT gorerajeev alabelledsequentcalculusforbbiprooftheoryandproofsearch AT tiualwen alabelledsequentcalculusforbbiprooftheoryandproofsearch AT houzhe labelledsequentcalculusforbbiprooftheoryandproofsearch AT gorerajeev labelledsequentcalculusforbbiprooftheoryandproofsearch AT tiualwen labelledsequentcalculusforbbiprooftheoryandproofsearch |