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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Dyckhoff, R., Kesner, D., & Lengrand, S. (2006). Strong Cut-elimination systems for Hudelmaier’s depth-bounded sequent calculus for implicational logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4130 LNAI, pp. 347–361). Springer Verlag. https://doi.org/10.1007/11814771_31
Mendeley helps you to discover research relevant for your work.