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
AI-powered service management for IT and enterprise teams
Give your IT, operations, and business teams the ability to deliver exceptional services—without the complexity. Maximize operational efficiency with refreshingly simple, AI-powered Freshservice.
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