Extracting Herbrand disjunctions by functional interpretation

DOI10.1007/S00153-005-0275-1MaRDI QIDQ2486989zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• On extracting variable Herbrand disjunctions
• A sequent-calculus based formulation of the extended first epsilon theorem
• On the Herbrand functional interpretation
• Herbrand's theorem and extractive proof theory
• A herbrandized functional interpretation of classical first-order logic

Cites work

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

Cited in

(20)

• A complexity analysis of functional interpretations
• A herbrandized functional interpretation of classical first-order logic
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• scientific article; zbMATH DE number 1950249 (Why is no real title available?)
• scientific article; zbMATH DE number 1841838 (Why is no real title available?)
• On extracting variable Herbrand disjunctions
• On the Herbrand functional interpretation
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Herbrand's theorem as higher order recursion
• Extracting Herbrand trees in classical realizability using forcing
• Herbrand complexity and the epsilon calculus with equality
• Herbrand's theorem and extractive proof theory
• On the practical value of Herbrand disjunctions
• Herbrand's theorem and term induction
• On the non-confluence of cut-elimination
• A sequent-calculus based formulation of the extended first epsilon theorem
• Herbrand analyses
• Herbrand Sequent Extraction
• On the Herbrand content of LK
• scientific article; zbMATH DE number 7533330 (Why is no real title available?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486989)