论文标题
裁切的消除和归一化，用于通用单一和多结论序列和自然扣除曲线
Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
论文作者
论文摘要
任何一组真理功能的连接器都具有依次的计算规则，可以从连接剂的真实表中系统地生成。这样的序列演算产生了多结论的自然扣除系统，并产生了Parigot的自由扣除版本。消除规则是“一般”，但可以系统地简化。切除和归一化。限制在成功中的单个公式会产生这些系统的直觉版本。该规则还产生了广义的lambda calculi，为自然扣除证明提供了证明术语，例如咖喱豆霍德同构中。间接证明规则的添加会产生这些系统的经典单缔合版本。 Gentzen的标准系统作为特殊情况出现。
Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot's free deduction. The elimination rules are "general," but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curry-Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen's standard systems arise as special cases.
