Studia Logica 60 (1):107-118 (1998)
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.
|Keywords||Cut-elimination normalisation natural deduction intuitionistic logic recursive path ordering termination|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
1999 Spring Meeting of the Association for Symbolic Logic.Charles Parsons - 1999 - Bulletin of Symbolic Logic 5 (4):479-484.
Similar books and articles
A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.Arnon Avron - unknown
Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.Linda Postniece - unknown
Added to index2009-01-28
Total downloads60 ( #84,931 of 2,152,625 )
Recent downloads (6 months)3 ( #225,818 of 2,152,625 )
How can I increase my downloads?