Proof Normalization Modulo

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. Deduction modulo [11] is a formulation of first-order logic, that gives a formal account of the difference between deduction and computation in mathematical proofs. In deduction modulo a theory is formed with a set of axioms and a congruence, often defined by a set of rewrite rules. For instance, when defining arithmetic in deduction modulo, we can either take the usual axiom x x+0 = x or orient this axiom as a rewrite rule x + 0 x, preserving provability. In the same way, when defining the theory of integral domains, we can chose to take the axiom x y (x

• Type: Conference
• Year: 1998
• Where: TYPES
• Authors: Gilles Dowek, Benjamin Werner
• Keywords: Cut Elimination, Deduction Modulo, Formal Methods, Rewrite Rules, TYPES 1998