Cut-elimination and proof schemata

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free