Writing programs that construct proofs

DOI10.1007/BF00244273zbMath0615.68063OpenAlexW2019651724MaRDI QIDQ1820596

J. L. Bates, T. B. Knoblock, Robert L. 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

LCFintelligent systemsautomated reasoningformal mathematicsdecision proceduresproof checkingAutomath

Mathematics Subject Classification ID

Related Items (5)

Innovations in computational type theory using Nuprl ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Do-it-yourself type theory ⋮ An intuitionistic theory of types with assumptions of high-arity variables ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Uses Software

• LCF

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