Proof normalization modulo

被引：42

作者：

Dowek, G ^{[1
]}

Werner, B ^{[1
]}

机构：

[1] Ecole Polytech, LIX, INRIA, F-91128 Palaiseau, France

来源：

JOURNAL OF SYMBOLIC LOGIC | 2003年 / 68卷 / 04期

关键词：

D O I：

10.2178/jsl/1067620188

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

引用

页码：1289 / 1316

页数：28

共 50 条

[1] Languages modulo normalization
Ohsaki, Hitoshi
Seki, Hiroyuki
FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 221 - +
[2] Inductive proof search modulo
Fabrice Nahon
Claude Kirchner
Hélène Kirchner
Paul Brauner
Annals of Mathematics and Artificial Intelligence, 2009, 55 : 123 - 154
[3] Inductive proof search modulo
Nahon, Fabrice
Kirchner, Claude
Kirchner, Helene
Brauner, Paul
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2009, 55 (1-2) : 123 - 154
[4] Normalization proof for Peano Arithmetic
Siders, Annika
ARCHIVE FOR MATHEMATICAL LOGIC, 2015, 54 (7-8) : 921 - 940
[5] ON PROOF NORMALIZATION IN LINEAR LOGIC
GALMICHE, D
PERRIER, G
THEORETICAL COMPUTER SCIENCE, 1994, 135 (01) : 67 - 110
[6] PROOF NORMALIZATION FOR RESOLUTION AND PARAMODULATION
BACHMAIR, L
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 355 : 15 - 28
[7] PROOF NORMALIZATION WITH NONSTANDARD OBJECTS
GOTO, S
THEORETICAL COMPUTER SCIENCE, 1991, 85 (02) : 333 - 351
[8] Normalization proof for Peano Arithmetic
Annika Siders
Archive for Mathematical Logic, 2015, 54 : 921 - 940
[9] Data width requirements in SISO decoding with modulo normalization
Wu, YF
Woerner, BD
Blankenship, TK
IEEE TRANSACTIONS ON COMMUNICATIONS, 2001, 49 (11) : 1861 - 1868
[10] Proof of a conjecture on a congruence modulo 243 for overpartitions
Xiaoqian Huang
Olivia X. M. Yao
Periodica Mathematica Hungarica, 2019, 79 : 227 - 235

← 1 2 3 4 5 →