HOL 7

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.

last updated on:
July 28th, 2012, 16:31 GMT
price:
FREE!
developed by:
Michael Norrish
license type:
BSD License 
category:
ROOT \ Programming \ Quality Assurance and Testing

FREE!

In a hurry? Add it to your Download Basket!

user rating

UNRATED
0.0/5
 

0/5

What's 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.
read full changelog

Add your review!

SUBMIT