In the fully expansive (or LCF-style) approach to theorem proving, theorems are represented by an abstract type whose primitive operations are the axioms and inference rules of a logic. Theorem proving tools are implemented by composing together the inference rules using ML programs. This idea can be generalised to computing valid judgements that represent other kinds of information. In particular, consider judgements (a,r,t,b), where a is a set of boolean terms (assumptions) that are assumed true, r represents a variable order, t is a boolean term all of whose free variables are boolean and b is a BDD. Such a judgement is valid if under the assumptions a, the BDD representing t with respect to r is b, and we will write a r t --> b when this is the case. The derivation of "theorems" like a r t --> b can be viewed as "proof" in the style of LCF by defining an abstract type term_bdd that models judgements a r t --> b analogously to the way the type thm models theorems |- t.
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 SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. several widely used versions of the HOL system: 1. HOL88 from Cambridge; 2. HOL90 from Calgary and Bell Labs; 3. HOL98 from Cambridge, Glasgow and Utah. HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL.
HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.
ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation...All the ProofPower packages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License. (PPDaz is Ada stuff)