Description
Interactive theorem prover based on Higher-Order Logic.
HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.