Talks and Poster Presentations (with Proceedings-Entry):
A. Leitsch, M. Baaz, A. Lolic:
"A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem";
Keynote Lecture: Logical Foundations of Computer Science - International Symposium, LFCS 2018,
Florida (invited);
01-08-2018
- 01-11-2018; in: "LNCS 10703",
Springer International Publishing AG,
10703
(2018),
55
- 71.
English abstract:
The optimal calculation of Herbrand disjunctions from unformalized or formalized mathematical proofs is one of the most prominent problems of computational proof theory. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbertīs epsilon formalism (which is in fact also the oldest framework for proof theory). The algorithm to calculate Herbrand disjunctions is an integral part of the proof of the extended first epsilon theorem. This paper connects epsilon proofs and sequent calculus derivations with cuts. This leads to an improved notation for the epsilon formalism and a computationally improved version of the extended first epsilon theorem, which allows a nonelementary speed-up of the computation of Herbrand disjunctions.
Keywords:
Extended first epsilon theorem, Herbrand disjunctions, Epsilon calculus
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-72056-2_4
Created from the Publication Database of the Vienna University of Technology.