The foundation of a generic theorem prover
From MaRDI portal
Publication:1823013
DOI10.1007/BF00248324zbMath0679.68173WikidataQ57382729 ScholiaQ57382729MaRDI QIDQ1823013
Publication date: 1989
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
LCF; higher-order logic; natural deduction; logical framework; higher-order unification; Standard ML; ISABELLE; meta reasoning
DB lookup for MSC labels failed
Related Items
Unnamed Item, Equivalences between logics and their representing type theories, Forum: A multiple-conclusion specification logic, Using typed lambda calculus to implement formal systems on a machine, Theo: An interactive proof development system, Program development in constructive type theory, Unification under a mixed prefix, Implementing tactics and tacticals in a higher-order logic programming language, Experimenting with Isabelle in ZF set theory, Set theory for verification. I: From foundations to functions, Inductive families, Program tactics and logic tactics, Proof-search in type-theoretic languages: An introduction, Program development schemata as derived rules, TPS: A theorem-proving system for classical type theory, Unnamed Item, A Shell for Generic Interactive Proof Search
Uses Software