Proof normalization modulo

Journal of Symbolic Logic 68 (4):1289-1316 (2003)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 91,202

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

60 (#256,806)

6 months
9 (#242,802)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
A Mathematical Introduction to Logic.Herbert Enderton - 2001 - Bulletin of Symbolic Logic 9 (3):406-407.
A Computational Logic.Robert S. Boyer & J. Strother Moore - 1990 - Journal of Symbolic Logic 55 (3):1302-1304.
Typed Lambda calculi. S. Abramsky et AL.H. P. Barendregt - 1992 - In S. Abramsky, D. Gabbay & T. Maibaurn (eds.), Handbook of Logic in Computer Science. Oxford University Press. pp. 117--309.

Add more references