HOL 3 review

HOL short from Higher Order Logic is a programming environment in which theorems can be proved and proof tools implemented. Built-

License: BSD License File size: 0K Developer: Michael Norrish

0

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:
This release adds theories of co-inductive (possibly infinite) labelled transition paths in pathTheory, and of sorting and list permutations in sortingTheory.
It adds a new first-order proof tactic (called METIS_TAC) that uses an ordered resolution and paramodulation, and a 'boolification' tool that automatically defines functions that map data types to boolean vectors.
Many extensions, bugfixes, and backwards incompatibilities.