# HOL Zero

## What is HOL Zero?

HOL Zero is a basic theorem prover for the HOL logic, designed with
trustworthiness as its top priority. It is primarily intended for two roles:

- A highly-trustworthy system for checking and/or consolidating proofs
created on other theorem provers;
- A pedagogical example of a simple theorem prover and its
implementation.

Note that some proof porting mechanism is required for the role of
checking/consolidating proofs. One such mechanism is under development at Proof
Technologies.

Unlike other HOL systems, HOL Zero is NOT primarily targetted at developing
proofs, although it is suitable for simple natural deduction proofs. It
concentrates on doing basic functionality well, and has relatively good term
parsing, pretty printing and error reporting. Its source code is very carefully
written and commented, and aims to be as simple and readable as possible. An
extensive glossary of HOL-related
terminology is provided as part of the user documentation.

## Download

A source tarball for the current version can be downloaded here:
holzero-0.6.3.tgz (released 2016-04-25).

The following are required to run HOL Zero:

- A Unix-like operating system and the bash shell;
- The OCaml
programming language (version >= 3.08);
- The Camlp5
extension to OCaml.

To get started using HOL Zero, unpack the downloaded tarball by entering
`tar -xzf holzero-0.6.3.tgz`

at a terminal window, then change to the
resulting `holzero-0.6.3`

directory and follow the instructions in
Sections 3 and 4 of the README file.

## Unsoundness Bounty

There is a $100 bounty reward for finding soundness-related flaws in HOL
Zero. See here for a list of unsoundnesses
and successful claims.

## Contact Us

Email
holzero@proof-technologies.com with any queries, comments or bounty claims,
or simply to tell us you exist. Please help us by mentioning the operating
system(s) you are using with HOL Zero.

To receive occasional news about HOL Zero, email
holnews@proof-technologies.com with "subscribe" in the subject field.