scientific article; zbMATH DE number 65537

zbMATH Open0754.03040MaRDI QIDQ4012886FDOQ4012886

Authors: Chet Murthy, Robert Constable 

Publication date: 27 September 1992

Title of this publication is not available (Why is that?)

Recommendations

• Exploring Computational Contents of Intuitionist Proofs
• Getting results from programs extracted from classical proofs
• The computational content of arithmetical proofs
• scientific article; zbMATH DE number 517083
• scientific article; zbMATH DE number 1354109
• Classical proofs as programs: how, what and why
• A note on the complexity of classical and intuitionistic proofs
• scientific article; zbMATH DE number 895269
• On the computational content of intuitionistic propositional proofs
• scientific article; zbMATH DE number 1678362

zbMATH Keywords

constructive proofsclassical proofsfragment of type theorygeneral method of extracting algorithms from classical proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Cited In (19)

• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Relating Classical Realizability and Negative Translation for Existential Witness Extraction
• On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
• Transfinite update procedures for predicative systems of analysis
• Automated constructivization of proofs
• Exploring Computational Contents of Intuitionist Proofs
• Classical extraction in continuation models
• From feasible proofs to feasible computations
• A short proof of the strong normalization of classical natural deduction with disjunction
• A translation characterizing the constructive content of classical theories
• Classical proofs as programs: how, what and why
• Programs from proofs using classical dependent choice
• Exploring the computational content of the infinite pigeonhole principle
• The computational content of Walras' existence theorem
• The computational content of classical arithmetic
• Programs with continuations and linear logic
• Refined program extraction from classical proofs
• Title not available (Why is that?)
• Uniform Heyting arithmetic

Uses Software

• Nuprl

This page was built for publication:

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