Projects / HOL


Higher Order Logic (HOL) 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.

Operating Systems

Recent releases

  •  28 Jul 2012 03:36

    Release Notes: 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.

    •  03 Jan 2011 20:50

      Release Notes: 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.

      •  16 Jul 2009 23:12

        Release Notes: There is now a Poly/ML implementation of HOL4 available for users on platforms other than Windows. Overloading can now target "syntactic patterns". The :string type is now an alias for :char list. Types can now be numerals. The finite cartesian product "array" type can now be written with square brackets. wordsLib now supports evaluation over non-standard word-sizes. Support for Unicode was added. Support for Patricia trees was added. Many other enhancements and bugfixes were made.

        •  14 Jan 2007 11:00

          Release Notes: 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.

          •  30 Jan 2006 04:15

            Release Notes: 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.


            Project Spotlight


            A Fluent OpenStack client API for Java.


            Project Spotlight

            TurnKey TWiki Appliance

            A TWiki appliance that is easy to use and lightweight.