HOL HOL is a programming environment in which theorems can be proved and proof tools implemented.
Download

HOL Ranking & Summary

HOL Tags

programming environment automated proof system theorems solver HOL proof

HOL Description

HOL is a programming environment in which theorems can be proved and proof tools implemented. HOL short from Higher Order Logic is a programming environment in which theorems can be proved and proof tools implemented.Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines.HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.What's New in This Release:· New set comprehension notation was added.· SML string notation was added.· Support for the XEmacs editor was added.· Case expressions may now include literals as patterns.· Inductive definitions are now made with respect to a varying monoset.· Types that use abbreviated patterns are printed in abbreviated form.· Support for rational numbers and fixed-length integers was added.· Bugs that prevented some components from compiling under GCC 4 were fixed.· Normalization in natural numbers and integers was fixed.· Handling of empty strings was fixed.

HOL Related Software