Light monotone Dialectica methods for proof mining

DOI10.1002/malq.200710093zbMath1182.03106OpenAlexW2114110304MaRDI QIDQ3184220

Mircea-Dan Hernest

Publication date: 14 October 2009

Published in: MLQ (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.200710093

zbMATH Keywords

monotone functional interpretationprogram extraction from proofsuniform quantifiers

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Functionals in proof theory (03F10)

Related Items

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Pointwise hereditary majorization and some applications
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Uniform Heyting arithmetic
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• On the axiom of extensionality – Part I
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• On the axiom of extensionality, Part II
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Refined program extraction from classical proofs