Title :
Strong normalization for second order classical natural deduction
Author_Institution :
Paris VII Univ., France
Abstract :
The strong normalization theorem for second-order classical natural deduction is proved. The method used is an adaptation of the one of reducibility candidates introduced in a thesis by J.Y. Girard (Univ. Paris 7, 1972) for second-order intuitionistic natural deduction. The extension to the classical case requires, in particular, a simplification of the notion of reducibility candidates
Keywords :
inference mechanisms; lambda calculus; reducibility candidates; second order classical natural deduction; second-order intuitionistic natural deduction; strong normalization theorem; Calculus; Filters; H infinity control; Logic programming;
Conference_Titel :
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-3140-6
DOI :
10.1109/LICS.1993.287602
