7 citations · 9 across the 7 of their papers we have counts for
8 papers
Schemata, Cyclic Proofs and Herbrand Systems
Alexander Leitsch, Anela Lolic, Stella Mahler
Inductive proofs can be represented by proof schemata, a formalism that represents infinite sequences of proofs by recursive definitions. Since proof schemata avoid the explicit ap…
Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics
Mariami Gamsakhurdia, Matthias Baaz, Anela Lolic
In 1928, Bernays and Schoenfinkel proved the decidability of prenex sentences whose matrices contain no function symbols, now known as the Bernays-Schoenfinkel (BS) class. We inves…
Towards an Analysis of Proofs in Arithmetic
Alexander Leitsch, Anela Lolić, Stella Mahler
Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found i…
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…
Epsilon Calculus Provides Shorter Cut-Free Proofs
Matthias Baaz, Anela Lolic
In this paper we show that cut-free derivations in the epsilon format of sequent calculus provide for a non-elementary speed-up w.r.t. cut-free proofs in usual sequent calculi in f…
First-Order Interpolation Derived from Propositional Interpolation
Matthias Baaz, Anela Lolic
This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions toget…
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…
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…