HOL Light is an interactive theorem prover and proof checker for formalising and proving mathematical theorems in higher-order logic. Written in OCaml, the software uses the OCaml toplevel as its front end.
The prover has a small logical core designed to maintain a high standard of correctness. It includes automated proof tools and extensive libraries of pre-proved results covering areas such as arithmetic, set theory, and real analysis.
This is free and open source software.
Key Features
- Interactive theorem proving and proof checking.
- Formal reasoning in higher-order logic.
- Small logical core designed for strong correctness guarantees.
- Automated tools help reduce the work required to construct proofs.
- Libraries of pre-proved mathematical theorems.
- Includes results covering arithmetic, basic set theory, and real analysis.
- Fully programmable and extensible using OCaml.
- Supports adding new theorems and inference rules without compromising soundness.
- Uses the OCaml toplevel as its interactive front end.
Website: github.com/jrh13/hol-light
Support:
Developer: John Harrison and contributors
License: BSD-2-Clause
HOL Light is written in OCaml. Learn OCaml 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. |