David Cerna, Michael Lettmann,
"Integrating a Global Induction Mechanism into a Sequent Calculus"
: TABLEAUX 2017, Springer, 9-2017
Original Titel:
Integrating a Global Induction Mechanism into a Sequent Calculus
Sprache des Titels:
Englisch
Original Buchtitel:
TABLEAUX 2017
Original Kurzfassung:
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.