Outil de traduction automatique permettant de convertir des fichiers au format Rec vers le format Dedukti. Ce projet facilite l'interopérabilité entre différents systèmes de preuve formelle, notamment pour la vérification de théorèmes en logique mathématique. Il s'adresse principalement aux chercheurs et développeurs travaillant dans le domaine de la démonstration automatique et de la logique formelle.

Ce projet propose une traduction automatique d'une partie de la bibliothèque HOL-Light vers le système Rocq. Il permet d'aligner des types et fonctions mathématiques entre ces deux environnements de preuve formelle, facilitant ainsi l'utilisation de théorèmes HOL-Light dans Rocq. L'objectif est d'accélérer le développement de preuves formelles en exploitant des résultats déjà établis dans HOL-Light, tout en garantissant leur compatibilité avec Rocq.

Ce projet fournit une traduction en Coq de la définition des nombres réels dans HOL-Light, en utilisant le type nat de Coq. Il permet de formaliser des concepts mathématiques avancés et de vérifier des preuves automatiquement. La bibliothèque est générée à partir de HOL-Light et peut être utilisée pour des développements formels en mathématiques ou en informatique théorique.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet d'utiliser des théorèmes et outils de HOL-Light dans l'écosystème Rocq, facilitant ainsi la vérification formelle et l'automatisation de preuves mathématiques. La traduction couvre des concepts comme la logique propositionnelle, la résolution, les modèles canoniques et les algorithmes de réécriture.

Ce projet propose une bibliothèque Rocq qui automatise la traduction des bibliothèques HOL-Light vers Rocq, permettant d'utiliser des théorèmes et fonctions mathématiques dans Rocq. Il facilite l'interopérabilité entre ces deux systèmes de preuve formelle en alignant types et fonctions, et offre un accès à plus de 20 000 théorèmes couvrant des domaines variés comme l'arithmétique, l'algèbre, l'analyse ou la topologie. Les preuves traduites sont fournies sous forme d'axiomes pour une utilisation rapide, avec la possibilité de régénérer et vérifier les preuves originales si nécessaire.