Proof Technologies Ltd (original) (raw)

Proof Technologies Ltd

Home |Software |Publications |Various |Contact Us

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.

We have written a paper about how HOL Zero overcomes classic problems suffered in other HOL systems' parsers and pretty printers.

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 enteringtar -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 our Unsoundnesses Page for a list of unsoundnesses and successful claims.

News

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