3 citations · 3 across the 3 of their papers we have counts for
4 papers
A Tableaux Calculus for Reducing Proof Size
Michael Peter Lettmann, Nicolas Peltier
A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are…
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…
The problem of Pi_2-cut-introduction
Alexander Leitsch, Michael Peter Lettmann
We describe an algorithmic method of proof compression based on the introduction of Pi_2-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen s c…