Commands in the package
hol-light
About hol-light
From Debian's package 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 aimed at the formalization of Tom Hales' proof of the Kepler conjecture.
From Debian's description of the hol-light package, under that package's license.
Dependencies
Depends on
camlp5camlp5-1t9p9libcamlp-streams-ocaml-dev-0lin0libcompiler-libs-ocaml-dev-gxzm3libstdlib-ocaml-dev-m4xw9libzarith-ocaml-dev-h79v1ocaml-5.3.0
On x86-64 it also needs camlp5-4new7 and libcompiler-libs-ocaml-dev-4b6d0, and does without camlp5-1t9p9 and libcompiler-libs-ocaml-dev-gxzm3.
Related apps
- z3theorem prover from Microsoft ResearchCommand line
- cvc4automated theorem prover for SMT problemsCommand line
- eproverEquational theorem proverCommand line
- monatheorem prover based on automataCommand line
- elantool for managing installations of the Lean theorem proverCommand line
- spassautomated theorem prover for first-order logic with equalityCommand line
Sources and licenses
- Name: the Debian package name.
- Summary: Debian's short description of the hol-light package, under that package's license.
- Description: Debian's description of the hol-light package, under that package's license.
- Versions and sizes: Debian's archive for ARM64, as on packages.debian.org.
- Popularity: Debian Popularity Contest counts.
More in About the catalog.