Exploring Computational Contents of Intuitionist Proofs

DOI10.1093/JIGPAL/JZI005MaRDI QIDQ5463274zbMATH OpenOpenAlexFDO

Authors Geiza M. Hamazaki da Silva, Edward Hermann Haeusler, Paulo A. S. Veloso

Publication date 3 August 2005

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzi005

zbMATH Keywords

Intuitionistic logicNatural deductionProgram synthesis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Recommendations

• On the computational content of intuitionistic propositional proofs
• Proof complexity of intuitionistic implicational formulas
• scientific article; zbMATH DE number 65537
• scientific article; zbMATH DE number 3976993
• Extracting Algorithms from Intuitionistic Proofs
• Proof and Computation: Perspectives for Mathematics, Computer Science, and Philosophy
• scientific article; zbMATH DE number 1231696
• A note on the complexity of classical and intuitionistic proofs
• On extracting computations from propositional proofs (a survey)
• scientific article; zbMATH DE number 1354095

Cited in

(5)

• Extracting Algorithms from Intuitionistic Proofs
• Grigori Mints and computer science
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• A computational glimpse at the Leibniz and Frege hierarchies
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time

This page was built for publication: Exploring Computational Contents of Intuitionist Proofs

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