By Gentzen’s famous Hauptsatz (the cut-elimination theorem) every proof in sequent calculus for first-order logic with cuts can be transformed into a cut-free proof; cut-free proofs are analytic and consist entirely of syntactic material of the end-sequent (the proven theorem). But in systems with induction rules, cut-elimination is either impossible or does not produce proofs with the subformula property. One way to overcome this problem is to formulate induction proofs as infinite sequences of proofs in a uniform way and to develop a method, which yields a uniform description of the corresponding cut-free proofs. We present such a formalism, as an alternative to systems with induction rules, and define a corresponding cut-elimination method (based on the CERES-method for first-order logic). The basic tools of proof theory, such as sequent- and resolution calculi are enriched with inductive definitions and schemata of terms, formulas, proofs, etc. We define a class of inductive proofs which can be transformed into this formalism and subjected to schematic cut-elimination.
Dunchev, C., Leitsch, A., Rukhaia, M., & Weller, D. (2015). Cut-elimination and proof schemata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8984, pp. 117–136). Springer Verlag. https://doi.org/10.1007/978-3-662-46906-4_8