Lower Bounds on Herbrand's Theorem
From MaRDI portal
Publication:4198750
DOI10.2307/2042682zbMath0411.03048OpenAlexW4254052460MaRDI QIDQ4198750
Publication date: 1979
Published in: Proceedings of the American Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2042682
Related Items (33)
The number of axioms ⋮ Ceres in intuitionistic logic ⋮ Andrews Skolemization may shorten resolution proofs non-elementarily ⋮ Unifying the model theory of first-order and second-order arithmetic via \(\mathrm{WKL}_0^\ast\) ⋮ A herbrandized functional interpretation of classical first-order logic ⋮ The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ On feasible numbers ⋮ Effective Skolemization ⋮ Herbrand complexity and the epsilon calculus with equality ⋮ On the compressibility of finite languages and formal proofs ⋮ Classical logic with partial functions ⋮ UNSOUND INFERENCES MAKE PROOFS SHORTER ⋮ Non-elementary speed-ups in logic calculi ⋮ Complexity of resolution proofs and function introduction ⋮ Cut-elimination and redundancy-elimination by resolution ⋮ Translation of resolution proofs into short first-order proofs without choice axioms ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ A complexity analysis of functional interpretations ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ On the form of witness terms ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Complexity of translations from resolution to sequent calculus ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results ⋮ Compressibility of Finite Languages by Grammars ⋮ Herbrand Sequent Extraction ⋮ Cut normal forms and proof complexity ⋮ The complexity of the disjunction and existential properties in intuitionistic logic ⋮ Streams and strings in formal proofs. ⋮ Logic with equality: Partisan corroboration and shifted pairing ⋮ Book review of: Matthias Baaz and Alexander Leitsch, Methods of cut-elimination ⋮ The epsilon calculus and Herbrand complexity
This page was built for publication: Lower Bounds on Herbrand's Theorem
