Abstract
There are two kinds of theorem provers for higher order logics: fully automatic (e.g. TPS and Leo) and user guided (e.g. HOL4, HOL Light, ProofPower, Isabelle/HOL, Coq, Nuprl and PVS). All the user guided systems, except PVS, are based on the LCF "fully expansive" approach invented by Robin Milner. PVS evolved from a different tradition that doesn't expand everything down to primitive inferences. The emphasis here is on user guided proof assistants, but future developments in automatic higher order proof methods are likely to be incorporated into these as the automatic methods available today are mainly propositional or first order. © 2008 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Gordon, M. (2008). Twenty years of theorem proving for HOLs past, present and future. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 1–5). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
