Paquet : hol-light (20231021-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-gqpk7

  Paquet indisponible

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

  Paquet indisponible

• dep: libcompiler-libs-ocaml-dev-3fdf0

  Paquet indisponible

• dep: libstdlib-ocaml-dev-058x2

  Paquet indisponible

• dep: ocaml-4.14.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	Taille du paquet	Espace occupé une fois installé	Fichiers
ppc64el	5 771,0 ko	45 473,0 ko	[liste des fichiers]