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.
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics. The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group