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 propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light en utilisant des outils dédiés. Il permet de mapper des types et fonctions de HOL-Light vers des constructions idiomatiques dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis comme axiomes pour optimiser les performances.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light dédiée à la logique. L'objectif est de permettre une utilisation idiomatique des types et fonctions de HOL-Light dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis sous forme d'axiomes pour optimiser les performances.

Eo2lp est un outil de traduction qui convertit les signatures et scripts de preuves du solveur cvc5 (Eunoia) vers le format LambdaPi, compatible avec l'écosystème Dedukti. Il permet de vérifier automatiquement des preuves générées par cvc5 dans un cadre formel dédié, assurant leur cohérence et leur réduction de type. Le projet cible un sous-ensemble spécifique de cvc5 et offre des fonctionnalités de benchmark pour évaluer la couverture et la fiabilité des traductions.

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.

Outil dédié à la traduction générique de théories dans le langage Dedukti, un système basé sur le λΠ-calcul modulo théorie. Il propose trois modèles de traduction : les morphismes de théorie, les relations logiques et les plongements de théorie. Ces fonctionnalités aident les utilisateurs à adapter des systèmes formels entre eux, facilitant ainsi la réutilisation et l'interopérabilité des preuves logiques.

Outil conçu pour simplifier des preuves formelles écrites en Lean en éliminant certaines égalités définitionnelles. Il facilite la traduction de ces preuves vers d'autres systèmes comme Coq tout en permettant une forme limitée d'extensionalité simulée dans Lean. Le projet s'appuie sur des traductions extensionales vers intensionales pour rendre les preuves plus portables et vérifiables.

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