HOL 7

A programming environment in which theorems can be proved and proof tools implemented

  Add it to your Download Basket!

 Add it to your Watch List!

0/5

Rate it!

What's new in HOL 7:

  • 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
send us
an update
LICENSE TYPE:
BSD License 
USER RATING:
UNRATED
  0.0/5
DEVELOPED BY:
Michael Norrish
HOMEPAGE:
hol.sourceforge.net
CATEGORY:
ROOT \ Programming \ Quality Assurance and Testing
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

#proof system #programming environment #theorems solver #HOL #proof #automated #programming

Add your review!

SUBMIT