A cut-free proof theory for boolean BI (via display logic)
File(s)DTR09-13.pdf (215.01 KB)
Published version
Author(s)
Brotherston, James
Type
Report
Abstract
We give a display calculus proof system for Boolean BI (BBI) based
on Belnap’s general display logic. We show that cut-elimination holds in
our system and that it is sound and complete with respect to the usual
notion of validity for BBI. We then show how to constrain proof search
in the system (without loss of generality) by means of a series of proof
transformations. By doing so, we gain some insight into the problem of
decidability for BBI.
on Belnap’s general display logic. We show that cut-elimination holds in
our system and that it is sound and complete with respect to the usual
notion of validity for BBI. We then show how to constrain proof search
in the system (without loss of generality) by means of a series of proof
transformations. By doing so, we gain some insight into the problem of
decidability for BBI.
Date Issued
2009-01-01
Citation
Departmental Technical Report: 09/13, 2009, pp.1-25
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
25
Journal / Book Title
Departmental Technical Report: 09/13
Copyright Statement
© 2009 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Article Number
09/13