Epsilon Calculus Provides Shorter Cut-Free Proofs
Logic
2024-01-18 v1
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.
Cite
@article{arxiv.2401.09183,
title = {Epsilon Calculus Provides Shorter Cut-Free Proofs},
author = {Matthias Baaz and Anela Lolic},
journal= {arXiv preprint arXiv:2401.09183},
year = {2024}
}