7 citations · 9 across the 7 of their papers we have counts for
Showing 2024Show all
2 papers · 1 filter
math.LO2024★ 2 cited
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…
math.LO2024
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…