We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed 'g-sequents,' which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of 'inference rule types' as sets of operations that act over such objects, and define 'abstract (sequent) calculi' as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any sequent-style proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top elements in lattices correspond to nested sequent systems, while bottom elements correspond to labeled sequent systems, and observe that top and bottom elements coincide with many known (cut-free) nested and labeled sequent systems for logics characterized by Horn properties.

翻译：我们提出了一种新颖的、与逻辑无关的框架，用于研究序列式证明系统，该框架涵盖了文献中出现的多种证明论形式体系及具体证明系统。特别地，我们引入了一种广义形式的序列，称为"g-序列"，将其视为典型根岑式序列的二元图结构。进而，我们将多种"推理规则类型"定义为作用于这些对象上的运算集，并将"抽象（序列）演算"定义为由一组g-序列与有限运算集构成的二元组。该方法允许我们在一般情境下分析特定推理规则类型间的相互作用，阐明在何种条件下某类规则可以被其他规则置换或模拟，且适用于任何符合该框架的序列式证明系统。我们利用这些置换与模拟结果，建立了通用的演算与证明转换算法，表明每个抽象演算可被有效转换为多项式等价的抽象演算格。我们确定了计算该格的复杂度，并计算了格内不同演算中证明与序列的相对规模。我们认识到格中顶元素对应于嵌套序列系统，而底元素对应于标记序列系统，并观察到顶元素与底元素恰好与许多已知的、由霍恩性质刻画逻辑的（免切）嵌套与标记序列系统一致。