Other Higher Order Logic Theorem-Proving Systems

There are three other systems implementing the same logic as HOL4: HOL Light, by John Harrison and written in OCaml; ProofPower, by Rob Arthan and written in SML; and HOL Zero, by Mark Adams and written in OCaml.

The HOL provided by the Isabelle system (often written “Isabelle/HOL”) is very similar to the higher order logic of HOL4, HOL Light and ProofPower, but has a type system with Haskell-like type-classes.

The PVS system has a type system with predicate sub-typing. Getting a term (formula, definition) to typecheck can require arbitrary amounts of work, but definitions are a deal more expressive.

The HOL-ω system implements a sophisticated type system (like that of System Fω) that also remains a superset of HOL4’s. In terms of implementation, the system is also a drop-in replacement for HOL4: all existing HOL4 scripts should continue to work as before in HOL-ω.

HOLs That Are Nothing to do With Theorem-Proving


Time-stamp: "Monday, 10 November 2014; 05:39 UTC (Michael Norrish)"