The Epsilon Calculus and Herbrand Complexity |
| |
Authors: | Georg Moser Richard Zach |
| |
Institution: | (1) Computational Logic Group, Institute of Computer Science, University of Innsbruck, Innsbruck, A-6020, Austria;(2) Department of Philosophy, University of Calgary, Calgary, AB T2N 1N4, Canada |
| |
Abstract: | Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator e x . Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure. |
| |
Keywords: | Hilbert's ε -calculus epsilon theorems Herbrand's theorem proof complexity |
本文献已被 SpringerLink 等数据库收录! |
|