ISSN:
1572-8730
Keywords:
Cut-elimination
;
normalisation
;
natural deduction
;
intuitionistic logic
;
recursive path ordering
;
termination
Source:
Springer Online Journal Archives 1860-2000
Topics:
Mathematics
,
Philosophy
Notes:
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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1005099619660
Permalink