@article {IOPORT.01661165,
    author       = {Dowek, Gilles},
    title        = {About folding-unfolding cuts and cuts modulo.},
    year         = {2001},
    journal      = {Journal of Logic and Computation},
    volume       = {11},
    number       = {3},
    issn         = {0955-792X},
    pages        = {419-429},
    publisher    = {Oxford University Press, Oxford},
    doi          = {10.1093/logcom/11.3.419},
    abstract     = {Introduction: In first-order natural deduction, a cut is a sequence formed with an introduction rule followed by an elimination rule. This notion can be extended to deal with the axioms of some theories, e.g. type theory, set theory, the Stratified Foundations,\dots However, we still do not have a general notion of cut that would apply to any first-order theory. In this note, we compare two notions of cut that can be defined for a fairly large number of theories: the notion of cut with a folding and an unfolding rule introduced by {\it D. Prawitz} [Natural deduction. A proof-theoretical study, Almqvist and Wiksell, Stockholm (1965; Zbl 0173.00205)] (called cut with a $\lambda$-introduction and a $\lambda$-elimination rule there) and used for several theories, and the notion of cut modulo proposed more recently [the author and {\it B. Werner}, Lect. Notes Comput. Sci. 1657, 62-77 (1999; Zbl 0944.03052)]. We show here that the notion of cut modulo subsumes the notion of cut with the folding and unfolding rules.},
    identifier   = {01661165},
}