Debian logoDebian Screenshots >

hol-light

HOL Light theorem prover

Description

HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL Light is famous for the verification of floating-point arithmetic as well as for the Flyspeck project, which aims at the formalization of Tom Hales' proof of the Kepler conjecture.

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.


Homepage

http://www.cl.cam.ac.uk/~jrh13/hol-light/


Statistics

1362 other people were interested in this package here. The newest known version of this software is 20190729-2+b1 (Information last updated about 6 hours ago.)