Classical BI: a logic for reasoning about dualising resources
Classical BI: a logic for reasoning about dualising resources
复制标题
DOI：
10.1145/1480881.1480923
复制
发表时间：
2009-01
期刊：
影响因子：
--
通讯作者：
J. Brotherston;Cristiano Calcagno
中科院分区：
文献类型：
--
作者：
J. Brotherston;Cristiano Calcagno
我们展示了如何扩展O'Hearn和Pym的逻辑束的影响，BI，经典的BI（CBI），其中的加法和乘法连接词的行为经典。具体来说，CBI是（命题）布尔BI的非保守扩展，包括假、否定和析取的乘法版本。我们给出了一个代数语义CBI，使我们自然地考虑资源模型的CBI中的每一个资源都有一个独特的对偶。然后，我们给出了一个切消除CBI证明系统，基于贝尔纳普的显示逻辑，并证明了这个证明系统的可靠性和完整性，我们的语义。
We show how to extend O'Hearn and Pym's logic of bunched implications, BI, to classical BI (CBI), in which both the additive and the multiplicative connectives behave classically. Specifically, CBI is a non-conservative extension of (propositional) Boolean BI that includes multiplicative versions of falsity, negation and disjunction. We give an algebraic semantics for CBI that leads us naturally to consider resource models of CBI in which every resource has a unique dual. We then give a cut-eliminating proof system for CBI, based on Belnap's display logic, and demonstrate soundness and completeness of this proof system with respect to our semantics.