Light monotone Dialectica methods for proof mining

DOI10.1002/MALQ.200710093MaRDI QIDQ3184220zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Computer Science Logic
• Light Dialectica revisited
• Bounded functional interpretation
• scientific article; zbMATH DE number 1215497
• Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory

Cites work

• scientific article; zbMATH DE number 5605127 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 3504946 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 1222925 (Why is no real title available?)
• scientific article; zbMATH DE number 1231647 (Why is no real title available?)
• scientific article; zbMATH DE number 2174396 (Why is no real title available?)
• scientific article; zbMATH DE number 1870414 (Why is no real title available?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• On the axiom of extensionality – Part I
• On the axiom of extensionality, Part II
• Pointwise hereditary majorization and some applications
• Refined program extraction from classical proofs
• Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation in the proof-system \texttt{MinLog}
• Uniform Heyting arithmetic
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(3)

• Lemma Mining over HOL Light
• scientific article; zbMATH DE number 7471663 (Why is no real title available?)
• Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation in the proof-system \texttt{MinLog}

This page was built for publication: Light monotone Dialectica methods for proof mining

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