HOL4 is an interactive theorem prover for classical higher-order logic. It provides a platform for formalising mathematics, verifying hardware and software, and developing custom proof tools.
The system follows the LCF approach, with theorems created through a small trusted kernel interface. HOL4 is primarily implemented in Standard ML and supports Poly/ML and Moscow ML.
This is free and open source software.
Key Features
- Uses classical higher-order logic with a typed lambda calculus.
- Small trusted kernel provides a foundation for checked proofs.
- Powerful tactic language for constructing interactive proofs.
- Extensive simplification and rewriting facilities.
- Libraries and theories for formal mathematics and verification.
- Supports hardware and software verification.
- Tools for constructing custom proof procedures.
- Holmake batch compiler for building HOL developments.
- Works with Poly/ML and Moscow ML.
- Includes manuals, online help, and example formal developments.
Website: github.com/HOL-Theorem-Prover/HOL
Support:
Developer: HOL4 Contributors
License: BSD-3-Clause
HOL4 is written in Standard ML. Learn Standard ML with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |