HOL

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 is new in this release:

• HolSmtLib now also supports Z3 proof reconstruction for goals that involve fixed-width words and a translation from HOL into SMT-LIB 2 format.
• HolQbfLib supports checking for both validity and invalidity of certificates for Squolem 2.02. wordsSyntax.mk_word_replicate computes the width of the resulting word when applied to a numeral and a fixed-width word.
• The system supports syntax for decimal fractions.
• This syntax maps to division terms of the form n / 10m.
• In the core system, this syntax is enabled for the real, rational, and complex theories.

What is new in version 6:

• The HolSmtLib library now supports proof reconstruction for the SMT solver Z3.
• Many type variables can now be parsed and printed as lower-case Greek letters.
• Bounded rewrites work better.
• Simplification of terms involving the EL operator is better.
• Improved support for bag operations.
• Syntax updates for things like the universal set.
• Other minor enhancements and bugfixes.