Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus

We prove confluence of two cut-elimination procedures for the implicational fragment of a standard intuitionistic sequent calculus. One of the cut-elimination procedures uses global proof transformations while the other consists of local ones. Both of them include permutation of cuts to simulate -reduction in an isomorphic image of the -calculus. We establish the confluence properties through a conservativity result on the cut-elimination procedures.

• Type: Conference
• Year: 2007
• Where: CIE
• Authors: Kentaro Kikuchi
• Keywords: Applied Computing, CIE 2007, Cut-elimination Procedures, Global Proof Transformations, Intuitionistic Sequent Calculus