8 citations · 24 across the 9 of their papers we have counts for
6 papers · 1 filter
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…
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…
Algorithmic Introduction of Quantified Cuts
Stefan Hetzl, Alexander Leitsch, Giselle Reis +1
We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms pres…
CERES for First-Order Schemata
Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia +1
The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is alw…