Download
HOL is a system for proving theorems in Higher Order Logic. It
comes with a large variety of existing theories formalising
various parts of mathematics and theoretical computer science.
Features
- Easy programmability
- Sophisticated decision procedures
- Powerful reasoning tools
Categories
MathematicsLicense
BSD LicenseFollow HOL theorem-proving system
Other Useful Business Software
Go from Code to Production URL in Seconds
Skip the Kubernetes configs. Cloud Run handles HTTPS, scaling, and infrastructure automatically. Two million requests free per month.
Rate This Project
Login To Rate This Project
User Reviews
-
There are no examples of anything. 1. A complete proof of a common theorem of mathematics. 2. A new theorem being created rather than using existing ones. 3. Translating a proof into normal mathematical notation. (This would show that it really works.) This should be built in. It would make the system infinitely better. How about the well-known proof that there are irrational X and Y such that X^Y (X to the power of Y) is rational? How about proving the square root of 2 is irrational? Is there any truth to HOL or is it just Big Speculation? Charlie Volkstorf
