8 citations · 24 across the 9 of their papers we have counts for
9 papers
Herbrand's Theorem in Refutation Schemata
Alexander Leitsch, Anela Lolic
An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, ca…
Schematic Refutations of Formula Schemata
David Cerna, Alexander Leitsch, Anela Lolic
Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define…
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…
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…
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]
David Cerna, Alexander Leitsch
The schematic CERES method [8] is a recently developed method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can…
Introducing Quantified Cuts in Logic with Equality
Stefan Hetzl, Alexander Leitsch, Giselle Reis +2
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of…