Imperial College London
Mr Lloyd Kamara

MrLloydKamara

Faculty of Engineering, Department of Computing

Computing Support Manager
 
 
 
//

Contact

 

+44 (0)20 7594 8400l.kamara Website

 
 
//

Location

 

305Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@techreport{Brotherston:2009:10.25561/95285,
author = {Brotherston, J},
booktitle = {Departmental Technical Report: 09/13},
doi = {10.25561/95285},
publisher = {Department of Computing, Imperial College London},
title = {A cut-free proof theory for boolean BI (via display logic)},
url = {http://dx.doi.org/10.25561/95285},
year = {2009}
}
Download

RIS format (EndNote, RefMan)

TY  - RPRT
AB  - We give a display calculus proof system for Boolean BI (BBI) basedon Belnap’s general display logic. We show that cut-elimination holds inour system and that it is sound and complete with respect to the usualnotion of validity for BBI. We then show how to constrain proof searchin the system (without loss of generality) by means of a series of prooftransformations. By doing so, we gain some insight into the problem ofdecidability for BBI.
AU  - Brotherston,J
DO  - 10.25561/95285
PB  - Department of Computing, Imperial College London
PY  - 2009///
TI  - A cut-free proof theory for boolean BI (via display logic)
T1  - Departmental Technical Report: 09/13
UR  - http://dx.doi.org/10.25561/95285
UR  - http://hdl.handle.net/10044/1/95285
ER  -
Download