[ Paquet source : hol-light ]
Paquet : hol-light (20190729-4 et autres)
Liens pour hol-light
Ressources Debian :
- Rapports de bogues
- Developer Information
- Journal des modifications Debian
- Fichier de licence
- Suivis des correctifs pour Debian
Télécharger le paquet source hol-light :
Responsables :
Ressources externes :
- Page d'accueil [www.cl.cam.ac.uk]
Paquets similaires :
démonstrateur de théorème HOL Light
HOL Light est un démonstrateur de théorème interactif pour la logique d’ordre supérieur avec un cœur logique très simple exécuté dans toplevel OCaml. HOL Light est célèbre pour la vérification de l’arithmétique en virgule flottante ainsi que pour le projet Flyspeck, qui se veut la formalisation de Tom Hales de sa preuve de la conjecture de Kepler.
Autres paquets associés à hol-light
|
|
|
|
-
- dep: camlp5
- préprocesseur et bel afficheur pour OCaml – version classique
-
- dep: camlp5-fue62
- paquet virtuel fourni par camlp5
-
- dep: ocaml-nox-4.11.1
- paquet virtuel fourni par ocaml-nox
-
- sug: coinor-csdp
- Software package for semidefinite programming (binaries)
-
- sug: dmtcp
- Paquet indisponible
-
- sug: libocamlgraph-ocaml-dev
- graph library for OCaml
-
- sug: maxima
- système de calcul formel - système de base
-
- sug: pari-gp
- système de calcul formel PARI/GP – exécutables
-
- sug: prover9
- Paquet indisponible
-
- sug: python
- Paquet indisponible
-
- sug: readline-editor
- paquet virtuel fourni par ledit, rlfe, rlwrap
Télécharger hol-light
| Architecture | Version | Taille du paquet | Espace occupé une fois installé | Fichiers |
|---|---|---|---|---|
| i386 | 20190729-4+b3 | 4 865,0 ko | 37 815,0 ko | [liste des fichiers] |