Journal of Symbolic Logic 62 (4):1461-1479 (1997)
We give two proofs of strong normalisation for second order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced in  for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Non-Strictly Positive Fixed Points for Classical Natural Deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.
Church–Rosser Property of a Simple Reduction for Full First-Order Classical Natural Deduction.Y. Andou - 2003 - Annals of Pure and Applied Logic 119 (1-3):225-237.
Call-by-Name Reduction and Cut-Elimination in Classical Logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1):38-65.
Strong Normalization of Classical Natural Deduction with Disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1):21-37.
The -Calculus.Herman Geuvers, Robbert Krebbers & James McKinna - 2013 - Annals of Pure and Applied Logic 164 (6):676-701.
Similar books and articles
Corrigendum to "Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction".Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (4):1415-1416.
Natural Deduction for First-Order Hybrid Logic.Torben BraÜner - 2005 - Journal of Logic, Language and Information 14 (2):173-198.
The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning.Michael Gabbay - unknown
A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Normal Natural Deduction Proofs (in Classical Logic).Wilfried Sieg & John Byrnes - 1998 - Studia Logica 60 (1):67-106.
A Framework for the Transfer of Proofs, Lemmas and Strategies From Classical to Non Classical Logics.Ricardo Caferra, Stéphane Demri & Michel Herment - 1993 - Studia Logica 52 (2):197 - 232.
A Short Introduction to Intuitionistic Logic.G. E. Mint͡s - 2000 - Kluwer Academic / Plenum Publishers.
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (3):851-859.
Added to index2009-01-28
Total downloads32 ( #153,601 of 2,143,562 )
Recent downloads (6 months)2 ( #280,273 of 2,143,562 )
How can I increase my downloads?
There are no threads in this forum
Nothing in this forum yet.