基于Horn规则的抽象证明论基础
Foundations for an Abstract Proof Theory in the Context of Horn Rules
AI总结：
本文提出了一种基于Horn规则的抽象证明论框架，通过定义广义序列和推理规则类型，建立了通用的证明转换算法，并展示了如何将抽象演算转换为多项式等价的格结构。
摘要：
我们介绍了一个新的、与逻辑无关的框架，用于研究序列式证明系统，该框架涵盖了文献中出现的各种证明论形式化和具体的证明系统。特别是，我们引入了一种广义的序列，称为'g-序列'，这些被看作是典型、哥德尔式序列的二元图。然后，我们定义了多种'推理规则类型'作为在这些对象上操作的运算集，并将'抽象（序列）演算'定义为由一组g-序列和一个有限运算集组成的对。我们的方法允许在一般情况下分析某些推理规则类型如何相互作用，展示在什么条件下特定类型的规则可以与或模拟其他规则，并适用于任何符合我们框架的序列式证明系统。然后，我们利用我们的置换和模拟结果来建立通用的演算和证明转换算法，证明每个抽象演算可以有效地转换为一个多项式等价抽象演算的格。我们确定计算此格的复杂性，并计算不同演算中的证明和序列的相对大小。我们认识到格中的顶和底元素对应于许多已知的深层推理嵌套序列系统和标签序列系统（分别）用于具有Horn性质的逻辑。
英文摘要：
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 multisequent 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 and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
