HOL Zero is a new, basic theorem prover for the HOL logic, designed with trustworthiness as its top priority. It is primarily intended for two roles:
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 sophisticated 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.
A source tarball for the latest version can be downloaded here: holzero-0.6.0.tgz (released 2013-01-31).
The following are required to run HOL Zero:
To get started using HOL Zero, unpack the downloaded tarball by entering
tar -xzf holzero-0.6.0.tgz at a terminal window, then change to the resulting
holzero-0.6.0 directory and follow the instructions in section 1 of the INSTALL file and section 4 of the README file.
There is a $100 bounty reward for finding soundness-related flaws in HOL Zero. See here for a list of unsoundnesses and successful claims.
Six printer soundness flaws were found last year, all discovered at Proof Technologies and now all corrected. Five of these flaws could be exploited to make it appear that the logic was unsound, and so would have qualified for $100 bounty rewards. However there were no claims. Come on you people, try harder!
Email firstname.lastname@example.org 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 email@example.com with "subscribe" in the subject field.