package hol_light

  1. Overview
  2. Docs
The HOL-Light interactive theorem prover

Install

Dune Dependency

Authors

Maintainers

Sources

Release-3.0.0.tar.gz
md5=6b7ece405efe5d891f547042d102f9ee
sha512=ffedba9a96cd0058a1ec74825c25b22f5b29117c2e7378715c5f8efc576e6008576b0649395e8f5fab8575f7f81f8816fb19a57c81413bc0d9e7d0c49b8a4c99

Description

HOL Light is a computer program written by John Harrison to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. There are a number of versions of HOL, going back to Mike Gordon’s work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.

This package will install hol.sh which will run OCaml REPL with HOL Light loaded. To use a compiled module of HOL Light, please install with the hol_light_module OPAM package.

Published: 18 Oct 2024

Dependencies (20)

  1. ledit
  2. zarith >= "1.5"
  3. camlp5 >= "8.0"
  4. ocaml >= "4.14.0"
  5. ledit
  6. camlp5 >= "7.14"
  7. num
  8. ocaml >= "4.10.0" & < "4.14.0"
  9. ledit
  10. camlp5 >= "7.11" & < "8.01"
  11. num
  12. ocaml >= "4.08.0" & < "4.10.0"
  13. ledit
  14. camlp5 >= "7.06" & < "7.15"
  15. num
  16. ocaml >= "4.06.1" & < "4.08.0"
  17. camlp5 >= "7.01" & <= "7.1"
  18. ocaml >= "4.04.0" & < "4.06.0"
  19. camlp5 >= "6.15" & <= "7.1"
  20. ocaml > "4.02.0" & < "4.04.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.