13 citations · 50 across the 19 of their papers we have counts for
5 papers · 1 filter
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…
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…
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…
Arithmetic, Infinite Trees, and Second-order Subsystems: Notes and Observations
David M. Cerna
Work in progress concerning alternative formalizations of arithmetic.
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]
David Cerna, Alexander Leitsch
In previous work, an attempt was made to apply the schematic CERES method [8] to a formal proof with an arbitrary number of Π 2 cuts (a recursive proof encapsulating the infinitary…