A translation characterizing the constructive content of classical theories

MaRDI QIDQ3408133zbMATH OpenFDO

Authors Matthias Baaz, Christian G. Fermüller

Publication date 24 February 2010

zbMATH Keywords

constructive proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• scientific article; zbMATH DE number 2174394
• scientific article; zbMATH DE number 65537
• Relating Classical Realizability and Negative Translation for Existential Witness Extraction
• Interpreting classical theories in constructive ones
• A realizability interpretation for classical analysis

Cited in

(7)

• A constructive valuation semantics for classical logic
• Automated constructivization of proofs
• scientific article; zbMATH DE number 2174394 (Why is no real title available?)
• scientific article; zbMATH DE number 1420833 (Why is no real title available?)
• Note on Conditional Constructivity
• scientific article; zbMATH DE number 4187806 (Why is no real title available?)
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• OilEd

This page was built for publication: A translation characterizing the constructive content of classical theories

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