Record link: 
http://hdl.handle.net/20.500.12708/223295
-
Title: 
Epsilon Calculus Provides Shorter Cut-Free Proofs
en
Citation: 
Baaz, M., & Lolić, A. (2025). Epsilon Calculus Provides Shorter Cut-Free Proofs. In K. Meer, A. Rabinovich, E. Ravve, & A. Villaveces (Eds.), Model Theory, Computer Science, and Graph Polynomials : Festschrift in Honor of Johann A. Makowsky (pp. 65–75). Birkhäuser. https://doi.org/10.1007/978-3-031-86319-6_7
-
Publisher DOI: 
10.1007/978-3-031-86319-6_7
-
Publication Type: 
Book Contribution - Edited Volume Contribution
en
Language: 
English
-
Authors: 
Baaz, Matthias 
Lolić, Anela 
-
Organisational Unit: 
E104-02 - Forschungsbereich Computational Logic 
E192-05 - Forschungsbereich Theory and Logic 
-
Published in: 
Model Theory, Computer Science, and Graph Polynomials : Festschrift in Honor of Johann A. Makowsky 
-
ISBN: 
978-3-031-86319-6
-
DOI of the book: 
10.1007/978-3-031-86319-6
-
Date (published): 
8-Mar-2025
-
Number of Pages: 
11
-
Publisher: 
Birkhäuser, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
Epsilon Calculus; Cut-Free Proofs; Sequent Calculus
en
Abstract: 
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 first-order language. In addition, a non-elementary speed-up is shown w.r.t. cut-free proofs in calculi with relaxed eigenvariable conditions which proved a speed-up themselves w.r.t. LK.
en
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 5%
1010 - Mathematik: 95%
-
Appears in Collections:
Book Contribution

Show full item record

Page view(s)

8
checked on Dec 29, 2025

Google ScholarTM

Check