Writing programs that construct proofs
From MaRDI portal
Publication:1820596
DOI10.1007/BF00244273zbMath0615.68063MaRDI QIDQ1820596
Robert L. Constable, T. B. Knoblock, J. L. Bates
Publication date: 1985
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
LCF; intelligent systems; automated reasoning; formal mathematics; decision procedures; proof checking; Automath
Related Items
Innovations in computational type theory using Nuprl, Do-it-yourself type theory, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, An intuitionistic theory of types with assumptions of high-arity variables
Uses Software