Proof normalization modulo
Gilles Dowek, Benjamin Werner · Journal of Symbolic Logic · 2003
Abstract 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.