RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC5528,
    author = {David M. Cerna and Anela Lolic},
    title = {{Proof Schemata for Theories equivalent to PA: on the Benefit of Conservative Reflection Principles}},
    language = {english},
    abstract = {Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and analysis can be quite difficult. Most alternative sequent calculus formalizations of induction do not extend Herbrand's theorem and are thus not fully adequate for proof analysis. In this work we extend the existing formalism of proof schemata, a recursive formulation of induction particularly suited for proof analysis, and show equivalence between PA and a fragment of our extended formalism. This relationship provides a conservative reflection principle between PA and an alternative proof formalism. A schematic approach need not be limited to arithmetic and should be investigated further. },
    year = {2018},
    month = {January },
    note = {In review},
    institution = {RISC},
    length = {22},
    url = {https://arxiv.org/abs/1711.10994}