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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
To represent the symmetry of LK we will work with critical \(\tau \)-formulas, i.e. \(A(\tau _x A(x)) \rightarrow A(t)\) represents \(\forall x A(x) \rightarrow A(t)\). This is only a notational convenience.
References
Aguilera, J.P., Baaz, M.: Unsound inferences make proofs shorter. CoRR, abs/1608.07703 (2016)
Andrews, P.B.: Resolution in type theory. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation (Artificial Intelligence), pp. 487–507. Springer, Heidelberg (1971). https://doi.org/10.1007/978-3-642-81955-1_29
Andrews, P.B.: Theorem proving via general matings. J. ACM (JACM) 28(2), 193–214 (1981)
Baaz, M., Hetzl, S., Weller, D.: On the complexity of proof deskolemization. J. Symbolic Logic 77(2), 669–686 (2012)
Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundamenta Informaticae 20(4), 353–379 (1994)
Baaz, M., Leitsch, A.: Cut normal forms and proof complexity. Ann. Pure Appl. Logic 97(1–3), 127–177 (1999)
Hilbert, D., Bernays, P.: Grundlagen der Mathematik II (1939)
Luckhardt, H.: Herbrand-analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, 234–263 (1989)
Moser, G., Zach, R.: The epsilon calculus and Herbrand complexity. Stud. Logica. 82(1), 133–155 (2006)
Acknowledgments
Partially supported by FWF grants P-26976-N25, I-2671-N35 and the Czech-Austrian project MOBILITY No. 7AMB17AT054.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Baaz, M., Leitsch, A., Lolic, A. (2018). A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science(), vol 10703. Springer, Cham. https://doi.org/10.1007/978-3-319-72056-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-72056-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72055-5
Online ISBN: 978-3-319-72056-2
eBook Packages: Computer ScienceComputer Science (R0)