hol2dk

Notoriété 21 %

Hol2dk est un outil permettant de traduire des preuves provenant de l'assistant de preuve HOL-Light vers d'autres assistants de preuve tels que Dedukti, Lambdapi et Coq. Il s'agit d'un projet open-source développé par l'équipe Deducteam.

Dépôt de code

https://github.com/Deducteam/hol2dk (nouvelle fenêtre)9 étoiles

Cas d'utilisation métiers

Traduction de preuves entre différents assistants de preuve
Preuve automatisée de théorèmes mathématiques

Organisation

Administration centrale
- Gouvernement (Premier ministre et ministères)
  - Ministère de l’Enseignement supérieur, de la Recherche et de l'Espace
    - Établissements d'enseignement supérieur et de recherche - Ministère chargé de l'Enseignement supérieur
      - École normale supérieure Paris-Saclay (organisation rattachée)

Description générée le lundi 18 mars 2024 à 00:14:35

D'autres initiatives de la même organisation

lambdapi
github.com/Deducteam/lambdapi
Logipedia
github.com/Deducteam/Logipedia
Agda2Dedukti
github.com/Deducteam/Agda2Dedukti
Zenon Modulo
github.com/Deducteam/zenon_modulo