Studia Logica 60 (1):107-118 (1998)

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.
Keywords Cut-elimination  normalisation  natural deduction  intuitionistic logic  recursive path ordering  termination
Categories (categorize this paper)
DOI 10.1023/A:1005099619660
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,316
Through your library

References found in this work BETA

Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
The Collected Papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam: North-Holland Pub. Co..
The Collected Papers of Gerhard Gentzen.K. Schütte - 1972 - Journal of Symbolic Logic 37 (4):752-753.

View all 11 references / Add more references

Citations of this work BETA

Advances in Proof-Theoretic Semantics.Peter Schroeder-Heister & Thomas Piecha (eds.) - 2015 - Cham, Switzerland: Springer Verlag.
1999 Spring Meeting of the Association for Symbolic Logic.Charles Parsons - 1999 - Bulletin of Symbolic Logic 5 (4):479-484.

Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
89 ( #132,489 of 2,519,496 )

Recent downloads (6 months)
1 ( #407,153 of 2,519,496 )

How can I increase my downloads?

Downloads

My notes