Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic

Abstract. Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicational case, thus strengthening existing approaches to Cut-admissibility. We decorate proofs with terms and introduce various term-reduction systems representing proof transformations. In contrast to previous papers which gave different arguments for Cut-admissibility suggesting weakly normalising procedures for Cut-elimination, our main reduction system and all its variations are strongly normalising, with the variations corresponding to different optimisations, some of them with good properties such as confluence.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Roy Dyckhoff, Delia Kesner, Stéphane Lengrand
• Keywords: Automated Reasoning, CADE 2006, Curry-Howard Correspondence, Intuitionistic Sequent Calculus, Various Term-reduction Systems