Proof Normalization Modulo

10 years 8 months ago
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
Gilles Dowek, Benjamin Werner
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Authors Gilles Dowek, Benjamin Werner
Comments (0)