Proof normalization modulo

Dowek, Gilles; Werner, Benjamin

J. Symbolic Logic, Tome 68 (2003) no. 1, p. 1289-1316 / Harvested from Project Euclid

Résumé

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.

Publié le : 2003-12-14
Classification:

@article{1067620188,
     author = {Dowek, Gilles and Werner, Benjamin},
     title = {Proof normalization modulo},
     journal = {J. Symbolic Logic},
     volume = {68},
     number = {1},
     year = {2003},
     pages = { 1289-1316},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1067620188}
}

Dowek, Gilles; Werner, Benjamin. Proof normalization modulo. J. Symbolic Logic, Tome 68 (2003) no. 1, pp.  1289-1316. http://gdmltest.u-ga.fr/item/1067620188/