In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any graph. We then provide sequent calculi operating on these formulas, we prove cut-elimination and that formula encoding the same graph are logically equivalent. We show that these systems provide conservative extensions of multiplicative linear logic (with and without mix) and classical propositional logic. We conclude by showing that one of these systems is equivalent to the graphical logic GS defined via a system of context-free graph rewiring rules, therefore providing an alternative proof of analyticity for this logic over graphs.

翻译：本文探讨在图上操作的相继式演算设计。为此，我们引入一组逻辑连接词，使得可将余图与经典命题公式之间的对应关系扩展至任意图。随后我们给出在这些公式上操作的相继式演算，证明切割消去性质，并证明编码同一图的公式在逻辑上等价。我们表明这些系统为乘法线性逻辑（含或不含混合规则）和经典命题逻辑提供了保守扩张。最后通过证明其中一个系统等价于由一组上下文无关图重写规则定义的图逻辑GS，从而为该图逻辑提供了另一种分析性证明。