Extracting Herbrand disjunctions by functional interpretation
From MaRDI portal
Publication:2486989
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
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
