Logic Beyond Formulas: A Proof System on Graphs
Logic Beyond Formulas: A Proof System on Graphs
复制标题
超越公式的逻辑：图的证明系统
DOI：
10.1145/3373718.3394763
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Lutz Straßburger
中科院分区：
文献类型：
--
作者：
Matteo Acclavio;Ross Horne;Lutz Straßburger
在本文中，我们提出了一个证明系统，操作图，而不是公式。我们开始我们的探索与著名的对应关系公式和余图，这是无向图，没有P4（四顶点路径）作为顶点诱导子图;然后我们放弃这个条件，看看任意（无向）图。结果是我们失去了对应于上图的公式的树结构。因此，我们不能使用依赖于树结构的标准证明理论方法。为了克服这个困难，我们使用了图的模块化分解和一些来自深度推理的技术，其中推理规则不依赖于公式的主连接符。对于我们的证明系统，我们展示了切割的容许性和分裂性质的推广。最后，我们证明了我们的系统是乘法线性逻辑（MLL）与混合的保守扩展，这意味着如果一个图是一个上图，并在我们的系统中可证明，那么它也是可证明的MLL+混合。
In this paper we present a proof system that operates on graphs instead of formulas. We begin our quest with the well-known correspondence between formulas and cographs, which are undirected graphs that do not have P4 (the four-vertex path) as vertex-induced subgraph; and then we drop that condition and look at arbitrary (undirected) graphs. The consequence is that we lose the tree structure of the formulas corresponding to the cographs. Therefore we cannot 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 generalization of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic (MLL) with mix, meaning that if a graph is a cograph and provable in our system, then it is also provable in MLL+mix.
超越公式作为图形：布尔逻辑到任意图形的扩展
DOI：
--
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Calk C
通讯作者：
Calk C