- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Strong normalization results by translation
Annals of Pure and Applied Logic 161 (9):1171-1179 (2010)
Abstract
We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.Links
PhilArchive
External links
(no proxy)
Setup an account with your affiliations in order to access resources via your University's proxy server
Through your library
- Sign in / register and customize your OpenURL resolver
- Configure custom resolver
My notes
Similar books and articles
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.
Natural deduction systems for some non-commutative logics.Norihiro Kamide & Motohiko Mouri - 2007 - Logic and Logical Philosophy 16 (2-3):105-146.
Strong Normalization Theorem for a Constructive Arithmetic with Definition by Transfinite Recursion and Bar Induction.Osamu Takaki - 1997 - Notre Dame Journal of Formal Logic 38 (3):350-373.
Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
Non deterministic classical logic: the $lambdamu^{++}$-calculus.Karim Nour - 2002 - Mathematical Logic Quarterly 48 (3):357-366.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Normalization without reducibility.René David - 2000 - Annals of Pure and Applied Logic 107 (1-3):121-130.
Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization.Ryo Takemura - 2013 - Studia Logica 101 (1):157-191.
Pragmatic normalization: Further results for some conjunctive and disjunctive sentences.Samuel Fillenbaum - 1974 - Journal of Experimental Psychology 102 (4):574.
Analytics
Added to PP
2013-12-18
Downloads
24 (#656,974)
6 months
14 (#179,578)
2013-12-18
Downloads
24 (#656,974)
6 months
14 (#179,578)
Historical graph of downloads
References found in this work
Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T.Felix Joachimski & Ralph Matthes - 2003 - Archive for Mathematical Logic 42 (1):59-87.
Proofs of strong normalisation for second order classical natural deduction.Michel Parigot - 1997 - Journal of Symbolic Logic 62 (4):1461-1479.
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.
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.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-64dd777598-cl5t5 uwo