Paquet : hol-light (1:3.0.0-2)

[ Paquet source : hol-light  ]

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-l2yh5

  paquet virtuel fourni par camlp5

• dep: libcamlp-streams-ocaml-dev-e0qf1

  paquet virtuel fourni par libcamlp-streams-ocaml-dev

• dep: libcompiler-libs-ocaml-dev-a6bv6

  paquet virtuel fourni par libcompiler-libs-ocaml-dev

• dep: libstdlib-ocaml-dev-bkvu1

  paquet virtuel fourni par libstdlib-ocaml-dev

• dep: libzarith-ocaml-dev-9lp69

  paquet virtuel fourni par libzarith-ocaml-dev

• dep: ocaml-5.2.0

  paquet virtuel fourni par ocaml

• sug: coinor-csdp

  paquet logiciel de programmation semi-définie – binaires

• 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

Télécharger pour toutes les architectures proposées

Architecture	Taille du paquet	Espace occupé une fois installé	Fichiers
i386	5 845,8 ko	45 967,0 ko	[liste des fichiers]