Strong Normalisation for a Gentzen-like Cut-Elimination Procedure

In this paper we introduce a cut-elimination procedure for classical logic, which is both strongly normalising and consisting of local proof transformations. Traditional cut-elimination procedures, including the one by Gentzen, are formulated so that they only rewrite neighbouring inference rules; that is they use local proof transformations. Unfortunately, such local proof transformation, if defined na¨ıvely, break the strong normalisation property. Inspired by work of Bloo and Geuvers concerning the λx-calculus, we shall show that a simple trick allows us to preserve this property in our cut-elimination procedure. We shall establish this property using the recursive path ordering by Dershowitz. Keywords. Cut-Elimination, Classical Logic, Explicit Substitution, Recursive Path Ordering.

• Type: Conference
• Year: 2001
• Where: TLCA
• Authors: Christian Urban
• Keywords: Classical Logic, Cut-elimination Procedure, Local Proof Transformation, Theoretical Computer Science, TLCA 2001