Email Gateway (Aug 22 2022 at 14:20): Email Gateway (Aug 22 2022 at 14:20):From: Mark Adams <mark@proof-technologies.com>
Hello Ken,
Not wanting to crowd your diagram too much, but I think maybe HOL Zero
(my system!) deserves a mention. It is a bare bones implementation of
the logic, and is designed to be highly trustworthy and robust.
http://www.proof-technologies.com/holzero.html
It can be used to create simple natural deduction proofs, but is mainly
intended as a proof checker to replay (via some proof recording
mechanism) formal proofs performed on other systems. It has
successfully replayed two quarters of the Flyspeck Project, for example,
that were originally performed in HOL Light in 1.4 billion primitive
inference steps. Another intended role is a pedagogical example of a
basic HOL system, with a simple coding style and lots of code comments
explaining what is going on, which also helps trustworthiness.
Mark Adams.
Last updated: Apr 18 2024 at 20:16 UTC