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 generalization 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 generalized connective.
翻译:在本文中,我们展示了一个以图表而不是公式操作的验证系统。 从公式和成文法之间众所周知的关系开始, 我们放下方言条件, 并查看任意的无方向的图形。 这意味着我们失去了与成文法相对应的公式的树结构, 我们不能再使用依赖该树结构的标准证明理论方法。 为了克服这一困难, 我们使用了图表的模块分解和从深度推论中得出的某些技术, 因为在这种推论中, 推断规则并不依赖于公式的主要连接。 对于我们的验证系统来说, 我们展示了分割属性的可接受性和普遍化。 最后, 我们展示了我们的系统是多种复制线性逻辑的保守扩展, 并结合了我们的论点是, 我们的图表形成了一种普遍连接的概念。