Strong normalization of classical natural deduction with disjunctions

This paper proves strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. By them, this paper also proves strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization. Key words: Classical natural deduction, Strong normalization, CPS-translation, Permutative conversion, General elimination

• Type: Journal
• Year: 2008
• Where: APAL
• Authors: Koji Nakazawa, Makoto Tatsuta
• Keywords: APAL 2008, Classical Natural Deduction, Natural Deduction, Strong Normalization