RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
  • @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}