一句话:提出直接在图上推理的证明系统,用模块分解与深推理证明 cut 可容许,并保守扩展 MLL+mix。
论文提出一种直接作用于图而非公式的证明系统。作者从公式与 cograph(不以 P4 为诱导子图的无向图)的经典对应出发,取消该限制,转向任意无向图。由于公式的树结构随之丢失,依赖树结构的标准证明论方法不再适用。为此,论文采用图的模块分解以及深推理技术,使推理规则不依赖公式主连接词。系统被证明具有 cut 可容许性,并满足分裂性质的推广。最后,作者证明该系统和带 mix 的乘法线性逻辑(MLL+mix)相比是保守扩张:若一个 cograph 在该系统中可证,则它在 MLL+mix 中也可证。
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.