一句话：提出一种在图而非公式上操作的分析性命题证明系统，利用图模块分解与深推理证明切可容许性，并保守扩展带 mix 的乘法线性逻辑。
本文提出一种在图上而非公式上操作的分析性命题证明系统。已有工作将公式与余图对应，但标准证明论方法通常依赖公式的树结构。作者放弃余图限制，转向任意无向图，从而失去树结构带来的便利。为克服困难，论文采用图的模块分解，并结合深推理（deep inference）技术，使推理规则不依赖公式的主连接词。系统被证明具有切可容许性（admissibility of cut）以及分裂性质（splitting property）的推广。最后，作者证明该系统是带 mix 的乘法线性逻辑（multiplicative linear logic with mix）的保守扩展，并论证这些图构成一种广义连接词（generalised connective）概念。
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.
@article{paperbot1647,
title = {An Analytic Propositional Proof System on Graphs},
author = {Matteo Acclavio and Ross Horne and Lutz Straßburger},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:1)2022}
}