Switch to: References

Add citations

You must login to add citations.
  1. Herbrand complexity and the epsilon calculus with equality.Kenji Miyamoto & Georg Moser - 2023 - Archive for Mathematical Logic 63 (1):89-118.
    The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...)
    Export citation