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
Keep company data safe with Chrome Enterprise
Make AI work your way with Chrome Enterprise. Block unapproved sites and set custom data controls that align with your company's policies.
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
