scientific article; zbMATH DE number 785043

MaRDI QIDQ4842532zbMATH OpenFDO

Authors Ulrich Berger, Helmut Schwichtenberg

Publication date 26 September 1995

zbMATH Keywords

natural deductionrecursioninductionexistential quantifierproof systemextracted program of a derivationfragment of minimal logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic programming (68N17) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 140006
• Extraction and verification of programs by analysis of formal proofs
• Program development in constructive type theory
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 1552509

Cited in

(8)

• Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms
• Completeness, minimal logic and programs extraction
• The greatest common divisor: A case study for program extraction from classical proofs
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• A logic program for transforming sequent proofs to natural deduction proofs
• scientific article; zbMATH DE number 140006 (Why is no real title available?)
• scientific article; zbMATH DE number 7471663 (Why is no real title available?)
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

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 Q4842532)