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 条

[1]

BELNAP ND, 1982, J PHILOS LOGIC, V11, P375

[2]

Berdine Josh, 2006, ENTCS

[3] Classical BI (A Logic for Reasoning about Dualising Resources) [J].

Brotherston, James ;

Calcagno, Cristiano .

ACM SIGPLAN NOTICES, 2009, 44 (01) :328-339

[4]

Brotherston James, 2010, P LICS 25 IN PRESS

[5] Deep inference and its normal form of derivations [J].

Bruennler, Kai .

LOGICAL APPROACHES TO COMPTATIONAL BARRIERS, PROCEEDINGS, 2006, 3988 :65-74

[6]

CALCAGNO C, 2007, P POPL 34

[7]

CHANG BYE, 2008, P POPL 35

[8]

CHIN WN, 2008, P POPL 35

[9] Bunched polymorphism [J].

Collinson, Matthew ;

Pym, David ;

Robinson, Edmund .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2008, 18 (06) :1091-1132

[10]

Distefano D, 2008, OOPSLA 2008 NASHVILLE, CONFERENCE PROCEEDINGS, P213

← 1 2 3 →