Strong normalization of classical natural deduction with disjunctions

DOI10.1016/J.APAL.2008.01.003zbMATH Open1141.03027OpenAlexW2043498337MaRDI QIDQ2482841FDOQ2482841

Authors Koji Nakazawa, Makoto Tatsuta 

Publication date 24 April 2008

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2008.01.003

zbMATH Keywords

strong normalizationpermutative conversion\(\lambda\mu\)-calculusCPS-translationgeneral elimination

Mathematics Subject Classification ID

Classical propositional logic (03B05) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Recommendations

• A note on strong normalization in classical natural deduction
• Strong normalization results by translation
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• A simple proof of second-order strong normalization with permutative conversions

Cites work

• scientific article; zbMATH DE number 1615235 (Why is no real title available?)
• scientific article; zbMATH DE number 1696602 (Why is no real title available?)
• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• scientific article; zbMATH DE number 2185662 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• A semantics of realisability for the classical propositional natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• A simple proof of second-order strong normalization with permutative conversions
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Call-by-value is dual to call-by-name
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Domain-free \(\lambda\mu\)-calculus
• Natural deduction with general elimination rules
• Non-strictly positive fixed points for classical natural deduction
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• Parallel reductions in \(\lambda\)-calculus
• Proofs of strong normalisation for second order classical natural deduction
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Stabilization -- an alternative to double-negation translation for classical natural deduction
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• Strong normalization proof with CPS-translation for second order classical natural deduction
• The duality of computation

Cited in

(16)

• scientific article; zbMATH DE number 1405618 (Why is no real title available?)
• Classical Logic with Mendler Induction
• Proofs of strong normalisation for second order classical natural deduction
• Strong normalization proof with CPS-translation for second order classical natural deduction
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• Peirce's rule in natural deduction.
• Strong normalization for truth table natural deduction
• Peirce's rule in a full natural deduction system
• A note on strong normalization in classical natural deduction
• Strong normalization proofs by CPS-translations
• A strong normalization result for classical logic
• A simple proof of second-order strong normalization with permutative conversions
• A short proof of the strong normalization of classical natural deduction with disjunction
• Proof Terms for Generalized Natural Deduction
• Strong normalization results by translation

This page was built for publication: Strong normalization of classical natural deduction with disjunctions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2482841)