3 papers
cs.LO2025
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…
cs.LO2025
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…
math.LO2020
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…