Paquet : hol-light (20230128-1 et autres)

[ 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-9wx53

  paquet virtuel fourni par camlp5

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

  paquet virtuel fourni par libcamlp-streams-ocaml-dev

• dep: ocaml-4.13.1

  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	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
ppc64el	20230128-1+b1	5 633,1 ko	43 544,0 ko	[liste des fichiers]