Order:
  1.  76
    Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
    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.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   6 citations