Skip to content

Latest commit

 

History

History

Formal_ineqs

A tool for verification of nonlinear inequalities in HOL Light

The most recent version of the tool is available here.

Part of the Flyspeck project: https://github.com/flyspeck/flyspeck

See docs/FormalVerifier.pdf for additional information.

Copyright / License

Except lib/ipow.hl, all files in this directory are copyright Alexey Solovyev 2014-2017. The file lib/ipow.hl is copyright Alexey Solovyev and the University of Utah 2014-2017.

Distributed under the same license as HOL Light (BSD-2-clause).