About folding-unfolding cuts and cuts modulo

被引：5

作者：

Dowek, G ^{[1
]}

机构：

[1] INRIA Rocquencourt, F-78153 Le Chesnay, France

来源：

关键词：

natural deduction; cut elimination; deduction modulo;

D O I：

10.1093/logcom/11.3.419

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We show in this note that cut elimination in deduction modulo subsumes cut elimination in deduction with the folding and unfolding rules.

引用

页码：419 / 429

页数：11

共 10 条

[1] RETRACTED: A NORMALIZATION THEOREM FOR SET-THEORY (Retracted article. See vol. 76, pg. 1096, 2011)
BAILIN, SC
[J]. JOURNAL OF SYMBOLIC LOGIC, 1988, 53 (03) : 673 - 695
[2] STRATIFICATION AND CUT-ELIMINATION
CRABBE, M
[J]. JOURNAL OF SYMBOLIC LOGIC, 1991, 56 (01) : 213 - 226
[3] CRABBE M, 1974, UNPUB
[4] DOWEK G, 1997, LECT NOTES COMPUTER, V1275, P105
[5] DOWEK G, 1998, UNPUB J AUTOMATED RE
[6] DOWEK G, 1999, LECT NOTES COMPUTER, V1657, P62
[7] EKMAN J, 1994, THESIS CHALMERS U TE
[8] Girard J-Y., 1990, PROOFS TYPES
[9] HALLNAS L, 1983, THESIS U STOCKHOLM
[10] PRAWITZ D, 1965, NATURAL DEDUCTION