@**inproceedings**{RISC5471,author = {David M. Cerna and Michael Lettmann},

title = {{Integrating a Global Induction Mechanism into a Sequent Calculus}},

booktitle = {{TABLEAUX 2017}},

language = {english},

abstract = {Most interesting proofs in mathematics contain an inductive argument
which requires an extension of the \textbf{LK}-calculus to formalize. The most
commonly used calculi contain a separate rule or axiom which
reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e.\ every formula
occurring in the proof is a subformula of the end sequent. Proof schemata are
a generalization of \textbf{LK}-proofs able to simulate induction by linking proofs, indexed by a natural number, together.
Using a global cut-elimination method a normal form can be reached which allows a schema of
{\em Herbrand Sequents} to be produced, an essential step for proof analysis in the presence of
induction. However, proof schema have only been studied in a limited context and are currently
defined for a very particular proof structure based on a slight extension of the \textbf{LK}-calculus. The result is an opaque and complex formalization. In this paper, we introduce
a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism. },

series = {lecture notes in computer science},

pages = {--},

publisher = {Springer},

isbn_issn = {KA},

year = {2017},

month = {September},

editor = {KA},

refereed = {yes},

length = {16},

conferencename = {Tableaux}

}