Writing programs that construct proofs

DOI10.1007/BF00244273MaRDI QIDQ1820596zbMATH OpenOpenAlexFDO

Authors T. B. Knoblock, J. L. Bates, Robert Constable

Publication date 1985

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00244273

zbMATH Keywords

LCFautomated reasoningdecision proceduresformal mathematicsproof checkingintelligent systemsAutomath

Mathematics Subject Classification ID

Recommendations

• Proofs and programs
• Proving and programming
• scientific article; zbMATH DE number 4006266
• Foreword to the special focus on formal proofs for mathematics and computer science
• A Proof-Theoretic Approach to Tactics

Cited in

(15)

• scientific article; zbMATH DE number 4101139 (Why is no real title available?)
• Formal proof of a program: find
• An overview of the Tecton proof system
• Meta programming on the proof level
• Tactic theorem proving with refinement-tree proofs and metavariables
• An intuitionistic theory of types with assumptions of high-arity variables
• Innovations in computational type theory using Nuprl
• scientific article; zbMATH DE number 549074 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• A computer environment for writing ordinary mathematical proofs
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Foreword to the special focus on formal proofs for mathematics and computer science
• Do-it-yourself type theory
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Programming as a mathematical exercise

Describes a project that uses

Uses Software

• LCF

This page was built for publication: Writing programs that construct proofs

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