Abstract. We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.
In REF , they furthermore propose a simplification of Herbelin's proof of strong cut-elimination for LJT .
Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.
Studia Logica
Mathematics Computer Science