A Unified Display Proof Theory for Bunched Logic

被引：11
作者：
Brotherston, James [1 ]
机构：
[1] Imperial Coll, Dept Comp, London, England
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2010年 / 265卷 / 0C期
基金：
英国工程与自然科学研究理事会;
关键词：
bunched logic; display calculus; proof theory; cut-elimination; substructural logic;
D O I：
10.1016/j.entcs.2010.08.012
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic seem very unlikely to exist.
引用
收藏
页码：197 / 211
页数：15
相关论文
共 24 条
[11]   The semantics of BI and resource tableaux [J].
Galmiche, D ;
Méry, D ;
Pym, D .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2005, 15 (06) :1033-1088
[12]  
GALMICHE D, 2006, P FSTTCS
[13]  
GORE R, 1998, LOG J IGPL, V0006, P00669
[14]  
Ishtiaq S., 2001, P POPL 28
[15]  
Kracht M, 1996, APPL LOG SER, V2, P93
[16]  
Larchey-Wendling Dominique, 2010, P LICS 25
[17]  
LARCHEY-WENDLING DOMINIQUE, 2009, MATH STRUCTURES COMP, V19, P1
[18]   The logic of bunched implications [J].
O'Hearn, PW ;
Pym, DJ .
BULLETIN OF SYMBOLIC LOGIC, 1999, 5 (02) :215-244
[19]  
Pym David, 2002, APPL LOGIC SERIES, DOI 10.1007/978-94-017-0091-7
[20]   Possible worlds and resources: The semantics of BI [J].
Pym, DJ ;
O'Hearn, PW ;
Yang, H .
THEORETICAL COMPUTER SCIENCE, 2004, 315 (01) :257-305
123