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，从而为这种图逻辑提供了分析性的替代证明。