Strong normalization proof with CPS-translation for second order classical natural deduction

&
Journal of Symbolic Logic 68 (3):851-859 (2003)
  Copy   BIBTEX

Abstract

This paper points out an error of Parigot’s proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,881

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Strong normalization of classical natural deduction with disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
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.
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.
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.
A semantical proof of the strong normalization theorem for full propositional classical natural deduction.Karim Nour & Khelifa Saber - 2006 - Archive for Mathematical Logic 45 (3):357-364.
A simple proof of second-order strong normalization with permutative conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
Strong normalization results by translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
Proofs of Strong Normalisation for Second Order Classical Natural Deduction.Michel Parigot - 1997 - Journal of Symbolic Logic 62 (4):1461-1479.
Proofs of strong normalisation for second order classical natural deduction.Michel Parigot - 1997 - Journal of Symbolic Logic 62 (4):1461-1479.
Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization.Ryo Takemura - 2013 - Studia Logica 101 (1):157-191.
An Alternative Normalization of the Implicative Fragment of Classical Logic.Branislav Boričić & Mirjana Ilić - 2015 - Studia Logica 103 (2):413-446.
A proof-theoretic investigation of a logic of positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.
The Faithfulness of Fat: A Proof-Theoretic Proof.Fernando Ferreira & Gilda Ferreira - 2015 - Studia Logica 103 (6):1303-1311.
A Normalization Procedure For The Equational Fragment Of Labelled Natural Deduction.A. de Oliveira & R. B. de Queiroz - 1999 - Logic Journal of the IGPL 7 (2):173-215.
Natural Deduction and Weak Normalization for Full Linear Logic.Lilia Martins & Ana Martins - 2004 - Logic Journal of the IGPL 12 (6):601-625.

Analytics

Added to PP
2009-01-28

Downloads
44 (#361,254)

6 months
16 (#157,007)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references