论文标题
图表上的分析命题证明系统
An Analytic Propositional Proof System on Graphs
论文作者
论文摘要
在本文中，我们提出了一个在图形上运行的证明系统，而不是公式。从公式和塞施仪之间的众所周知的关系开始，我们删除了Cophaph条件，并查看任意的无向图）。这意味着我们失去了与Cographs相对应的公式的树结构，并且我们无法再使用取决于该树结构的标准证明理论方法。为了克服这一困难，我们使用图形的模块化分解以及从深度推理中的某些技术，其中推理规则不依赖公式的主要结合。对于我们的证明系统，我们显示了削减的可采性和对分裂属性的概括。最后，我们表明我们的系统是与混合物的乘法线性逻辑的保守扩展，我们认为我们的图形构成了广义结缔组织的概念。
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.
