Ribbon Proofs - A Proof System for the Logic of Bunched Implications
Ribbon Proofs - A Proof System for the Logic of Bunched Implications
复制标题
Ribbon Proofs - 捆绑蕴涵逻辑的证明系统
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Julian Michael Lewis Bean
中科院分区：
文献类型：
--
作者：
Julian Michael Lewis Bean
在本论文中，我们提出了带状证明，即 Py m 和 O’Hearn 的捆绑蕴涵逻辑 (BI) 的证明系统。我们描述了该系统的两个关键动机。首先，现有的 BI 证明理论按照 Gentzen 的 LJ 风格进行序列化；没有现有的证明系统可以像 Gentzen 的 NJ 那样在单个公式的层面上发挥作用。其次，我们认为BI现有的证明系统中的证明并没有公正地对待空间性和资源的强烈语义概念，而这些概念对于逻辑本身的研究来说是如此令人兴奋的动机。我们首先将丝带校样非正式地作为图形系统呈现。然后，我们继续精确地形式化该系统，论文的主要结果是证明其相对于现有 BI 证明概念的健全性和完整性。我们讨论了形式化的一些性质及其与 BI 模型理论的关系，并形式化了系统中产生的一些几何直觉。我们提出了系统的扩展，用于证明程序逻辑论文中的一些实际结果，最后在机器学习中实现了系统的骨架，这有助于形式化的开发。 2006年提交伦敦大学玛丽皇后学院哲学博士学位
In this thesis we present ribbon proofs, a proof system for Py m and O’Hearn’s Logic of Bunched Implications (BI ). We describe two key motivations for the system. Firstly, t he existing proof theory forBI is sequentialized in the style of Gentzen’s LJ; there is no ex isting proof system which works on the level of individual formulae like Gentzen ’s NJ. Secondly, we believe that proofs inBI ’s existing proof systems do not do justice to the strong sema ntic notions of spatiality and resource which are such exciting motiviations for the st udy of the logic itself. We present ribbon proofs first informally as a graphical syst em. We then go on to formalize the system precisely, the main result of the thesis being the proof of its soundness and completeness relative to existing notions of proof for BI . We discuss some properties of our formalization and its relation toBI ’s model theory, and make formal a few geometric intuitions a ri ing from the system. We present an extension of the system used to prov e some real-world results from a paper in program logic, and finally a skeletal implementati on of the system in ML which was instrumental in the development of the formalization. Submitted for the degree of Doctor of Philosophy Queen Mary, University of London 2006