A Unified Display Proof Theory for Bunched Logic
A Unified Display Proof Theory for Bunched Logic
复制标题
DOI：
10.1016/j.entcs.2010.08.012
复制
发表时间：
2010-09-06
影响因子：
--
通讯作者：
Brotherston, James
中科院分区：
文献类型：
--
作者：
Brotherston, James
我们通过结合组件逻辑的显示演算，为四种主要的束逻辑类型制定了统一的显示演算证明理论。我们的演算满足删减法，并且就其标准表示而言是健全且完整的。我们表明，BI 的标准顺序演算可以看作是其显示演算的重新表述，并认为其他类型的成束逻辑的类似顺序演算似乎不太可能存在。
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.