基于Horn规则的抽象证明理论基础

我们引入了一种新颖的、逻辑无关的框架用于研究相继式风格证明系统，其涵盖文献中出现的大量证明论形式体系与具体证明系统。特别地，我们引入了一种广义相继式，称为“g-相继式”，其被视为典型Gentzen风格相继式的二元图。随后，我们将多种“推理规则类型”定义为作用于此类对象上的操作集合，并将“抽象（相继式）演算”定义为由一个g-相继式集合与一个有限操作集合组成的对。我们的方法允许在一般设定下分析特定推理规则类型如何相互作用，展示特定类型规则在何种条件下可与其他规则置换或被其模拟，且适用于任何契合本框架的相继式风格证明系统。我们进而利用置换与模拟结果建立通用的演算与证明变换算法，表明每个抽象演算均可被有效地变换为一个由多项式等价抽象演算构成的格。我们确定了计算该格的复杂度，并计算出格中不同演算内证明与相继式的相关大小。我们认识到，格中的顶元素与底元素分别对应于许多已知的深度推理嵌套相继式系统与标记相继式系统，用于由Horn性质刻画的逻辑。