7 citations · 9 across the 7 of their papers we have counts for
4 papers · 1 filter
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…
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…