<div class="csl-bib-body">
<div class="csl-entry">Baaz, M., & Lolić, A. (2025). Epsilon Calculus Provides Shorter Cut-Free Proofs. In K. Meer, A. Rabinovich, E. Ravve, & A. Villaveces (Eds.), <i>Model Theory, Computer Science, and Graph Polynomials : Festschrift in Honor of Johann A. Makowsky</i> (pp. 65–75). Birkhäuser. https://doi.org/10.1007/978-3-031-86319-6_7</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/223295
-
dc.description.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
dc.language.iso
en
-
dc.subject
Epsilon Calculus
en
dc.subject
Cut-Free Proofs
en
dc.subject
Sequent Calculus
en
dc.title
Epsilon Calculus Provides Shorter Cut-Free Proofs
en
dc.type
Book Contribution
en
dc.type
Buchbeitrag
de
dc.relation.isbn
978-3-031-86319-6
-
dc.relation.doi
10.1007/978-3-031-86319-6
-
dc.relation.issn
2297-024X
-
dc.description.startpage
65
-
dc.description.endpage
75
-
dc.type.category
Edited Volume Contribution
-
dc.relation.eissn
2297024X
-
tuw.booktitle
Model Theory, Computer Science, and Graph Polynomials : Festschrift in Honor of Johann A. Makowsky
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Trends in Mathematics
-
tuw.relation.publisher
Birkhäuser
-
tuw.relation.publisherplace
Cham
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E104-02 - Forschungsbereich Computational Logic
-
tuw.publication.orgunit
E192-05 - Forschungsbereich Theory and Logic
-
tuw.publisher.doi
10.1007/978-3-031-86319-6_7
-
dc.description.numberOfPages
11
-
tuw.author.orcid
0000-0002-7815-2501
-
tuw.editor.orcid
0009-0009-6367-2422
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
5
-
wb.sciencebranch.value
95
-
item.grantfulltext
none
-
item.languageiso639-1
en
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_3248
-
item.fulltext
no Fulltext
-
item.openairetype
book part
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.dept
E192-05 - Forschungsbereich Theory and Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie
