Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Pinyin
i2Cantonese
i2Cangjie
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TYPES

1998

Springer

1998

Springer

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

Related Content

Added |
06 Aug 2010 |

Updated |
06 Aug 2010 |

Type |
Conference |

Year |
1998 |

Where |
TYPES |

Authors |
Gilles Dowek, Benjamin Werner |

Comments (0)