Cographs are a class of (undirected) graphs, characterized by the absence of induced subgraphs isomorphic to the four-vertices path, showing an intuitive one-to-one correspondence with classical propositional formulas. In this paper we study sequent calculi operating on graphs, as a generalization of sequent calculi operating on formulas, therefore on cographs. We mostly focus on sequent systems with multiplicative rules (in the sense of linear logic, that is, linear and context-free rules) extending multiplicative linear logic with connectives allowing us to represent modular decomposition of graphs by formulas, therefore obtaining a representation of a graph with linear size with respect to the number of its vertices. We show that these proof systems satisfy basic proof theoretical properties such as initial coherence, cut-elimination and analyticity of proof search. We prove that the system conservatively extend multiplicative linear logic with and without mix, and that the system extending the former derives the same graphs which are derivable in the deep inference system GS from the literature. We provide a syntax for proof nets for our systems by extending the syntax of Retor\'e's RB-structures to represent graphical connectives. A topological characterization of those structures encoding correct proofs is given, as well as a sequentialization procedure to construct a derivation from a correct structure. We conclude the paper by discussing how to extend those linear systems with the structural rules of weakening and contraction, providing a sequent system for an extension of classical propositional logic beyond cographs.

翻译：余图是一类（无向）图，其特征是不存在与四顶点路径同构的诱导子图，并与经典命题公式存在直观的一一对应关系。本文研究以图为基础的相继式演算，作为以公式（从而以余图）为基础的相继式演算的推广。我们主要关注具有乘法规则（在线性逻辑的意义下，即线性和上下文无关规则）的相继式系统，通过引入连接词扩展乘法线性逻辑，使我们能够用公式表示图的模分解，从而得到与顶点数呈线性大小的图表示。我们证明这些证明系统满足基本证明论性质，如初始一致性、切割消除和证明搜索的分析性。我们证明该系统保守地扩展了含与不含混合运算的乘法线性逻辑，且扩展前者的系统推导出与文献中深入推理系统GS相同的图。通过扩展Retoré的RB结构语法以表示图形连接词，我们为系统提供了证明网语法。给出了编码正确证明的结构的拓扑特征刻画，以及从正确结构构造推导的序列化过程。最后，我们讨论如何用弱化和收缩的结构规则扩展这些线性系统，为超越余图的经典命题逻辑扩展提供相继式系统。