Extracting Herbrand disjunctions by functional interpretation

DOI10.1007/S00153-005-0275-1zbMath1081.03056OpenAlexW2082381286MaRDI QIDQ2486989

Philipp Gerhardy, Ulrich Kohlenbach

Publication date: 17 August 2005

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-005-0275-1

zbMATH Keywords

Herbrand's theoremfunctional interpretationHerbrand terms

Mathematics Subject Classification ID

Classical first-order logic (03B10) Functionals in proof theory (03F10)

Related Items (11)

On extracting variable Herbrand disjunctions ⋮ A herbrandized functional interpretation of classical first-order logic ⋮ On the Herbrand content of LK ⋮ Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language ⋮ Herbrand complexity and the epsilon calculus with equality ⋮ Unnamed Item ⋮ Herbrand's theorem as higher order recursion ⋮ Unnamed Item ⋮ A complexity analysis of functional interpretations ⋮ On the non-confluence of cut-elimination ⋮ Herbrand Sequent Extraction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A complexity analysis of functional interpretations
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed λ-calculus
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Lower Bounds on Herbrand's Theorem
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Computer Science Logic
• A note on Spector's quantifier-free rule of extensionality
• Logical problems of functional interpretations

This page was built for publication: Extracting Herbrand disjunctions by functional interpretation