A semantical proof of the strong normalization theorem for full propositional classical natural deduction

被引：7

作者：

Nour, K ^{[1
]}

Saber, K ^{[1
]}

机构：

[1] Univ Chambery, Equipe Log, LAMA, F-73376 Le Bourget Du Lac, France

来源：

ARCHIVE FOR MATHEMATICAL LOGIC | 2006年 / 45卷 / 03期

关键词：

Mathematical Logic; Classical Case; Natural Deduction; Strong Normalization; Normalization Theorem;

D O I：

10.1007/s00153-005-0314-y

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.

引用

页码：357 / 364

页数：8

共 27 条

[1] A semantical proof of the strong normalization theorem for full propositional classical natural deduction
Karim Nour
Khelifa Saber
Archive for Mathematical Logic, 2006, 45 : 357 - 364
[2] The Deduction Theorem for Strong Propositional Proof Systems
Beyersdorff, Olaf
THEORY OF COMPUTING SYSTEMS, 2010, 47 (01) : 162 - 178
[3] A short proof of the strong normalization of classical natural deduction with disjunction
David, R
Nour, K
JOURNAL OF SYMBOLIC LOGIC, 2003, 68 (04) : 1277 - 1288
[4] The Deduction Theorem for Strong Propositional Proof Systems
Olaf Beyersdorff
Theory of Computing Systems, 2010, 47 : 162 - 178
[5] The deduction theorem for strong propositional proof systems - (Extended abstract)
Beyersdorff, Olaf
FSTTCS 2007: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2007, 4855 : 241 - 252
[6] Strong normalization of classical natural deduction with disjunction
de Groote, P
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2001, 2044 : 182 - 196
[7] Strong normalization of classical natural deduction with disjunctions
Nakazawa, Koji
Tatsuta, Makoto
ANNALS OF PURE AND APPLIED LOGIC, 2008, 153 (1-3) : 21 - 37
[8] A note on strong normalization in classical natural deduction
Santo, Jose Espirito
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (213): : 41 - 51
[9] Strong normalization proof with CPS-translation for second order classical natural deduction
Kakazawa, K
Tatsuta, M
JOURNAL OF SYMBOLIC LOGIC, 2003, 68 (03) : 851 - 859
[10] Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
Ferrari, Mauro
Fiorentini, Camillo
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015), 2015, 9323 : 237 - 252

← 1 2 3 →