Article ID Journal Published Year Pages File Type
4662702 Annals of Pure and Applied Logic 2010 9 Pages PDF
Abstract

We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.

Related Topics
Physical Sciences and Engineering Mathematics Logic