Semantic Cut Elimination in the Intuitionistic Sequent Calculus
Semantic Cut Elimination in the Intuitionistic Sequent Calculus
复制标题
直觉序贯演算中的语义剪切消除
DOI：
10.1007/11417170_17
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
O. Hermant
中科院分区：
文献类型：
--
作者：
O. Hermant
割消元是证明理论的核心结果。本文提出了一种新的方法来证明Gentzen的直觉演算LJ的定理，它依赖于Kripke模型的无割演算的完备性。证明定义了一个通用的框架，以扩展切割消除结果到其他直觉演绎系统，特别是演绎模重写系统验证的一些性质。我们还给出了一个重写系统的示例，该重写系统适用削减消除，但不享受证明规范化。
Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen's intuitionistic sequent calculus LJ, that relies on completeness of the cut-free calculus with respect to Kripke Models. The proof defines a general framework to extend the cut elimination result to other intuitionistic deduction systems, in particular to deduction modulo provided the rewrite system verifies some properties. We also give an example of rewrite system for which cut elimination holds but that doesn't enjoys proof normalization.