13 citations · 50 across the 19 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
math.LO2017
Proof Schemata for Theories equivalent to : on the Benefit of Conservative Reflection Principles
David M. Cerna, Anela Lolic
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 anal…
math.LO2017
Integrating a Global Induction Mechanism into a Sequent Calculus
David M. Cerna, Michael Peter Lettmann
Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi for induction conta…
math.LO2017
Clausal Analysis of First-order Proof Schemata
David M. Cerna, Michael Lettmann
Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called proof links to the standard first-order LK-calculus. P…