A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem

  • Matthias Baaz
  • Alexander Leitsch
  • Anela LolicEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


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.


Extended first epsilon theorem Herbrand disjunctions Epsilon calculus 



Partially supported by FWF grants P-26976-N25, I-2671-N35 and the Czech-Austrian project MOBILITY No. 7AMB17AT054.


  1. 1.
    Aguilera, J.P., Baaz, M.: Unsound inferences make proofs shorter. CoRR, abs/1608.07703 (2016)Google Scholar
  2. 2.
    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). CrossRefGoogle Scholar
  3. 3.
    Andrews, P.B.: Theorem proving via general matings. J. ACM (JACM) 28(2), 193–214 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Baaz, M., Hetzl, S., Weller, D.: On the complexity of proof deskolemization. J. Symbolic Logic 77(2), 669–686 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundamenta Informaticae 20(4), 353–379 (1994)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Baaz, M., Leitsch, A.: Cut normal forms and proof complexity. Ann. Pure Appl. Logic 97(1–3), 127–177 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Hilbert, D., Bernays, P.: Grundlagen der Mathematik II (1939)Google Scholar
  8. 8.
    Luckhardt, H.: Herbrand-analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, 234–263 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Moser, G., Zach, R.: The epsilon calculus and Herbrand complexity. Stud. Logica. 82(1), 133–155 (2006)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Institute of Discrete Mathematics and Geometry 104TU WienViennaAustria
  2. 2.Institute of Computer Languages (E185)TU WienViennaAustria

Personalised recommendations