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 = {278--294},
publisher = {Springer},
isbn_issn = {978-3-319-66901-4},
year = {2017},
month = {September},
editor = {Renate A. Schmidt and Cl{\'{a}}udia Nalon},
refereed = {yes},
length = {16},
conferencename = {Tableaux}