Owner: michaeln

Category: Application

Proof assistant for higher order logic

Ultimately deriving from Gordon's HOL88, HOL4 is the latest version of this interactive theorem-proving system. It supports a tactic-based approach to proof, using the LCF approach that led to ML's invention as a programming language.

Dependencies: None

Platform: Linux, MacOS, Windows with Cygwin or WSL

Poly/ML version: >5.7.1

Licence: BSD

Download link: https://github.com/HOL-Theorem-Prover/HOL/archive/kananaskis-13.tar.gz

Project link: https://hol-theorem-prover.org