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.
Metis is an automatic theorem prover for first order logic with equality. Features of Metis * Coded in Standard ML (SML), with an emphasis on keeping the code as simple as possible. * Compiled using MLton to give respectable performance on standard benchmarks. * Reads in problems in the standard .tptp file format of the TPTP problem set. * Outputs detailed proofs in TSTP format, where each proof step is one of 6 simple rules. * Outputs saturated clause sets when input problems are discovered to be unprovable. Project Status Metis is being actively developed