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 bibliothèque Rocq (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet de manipuler des types et fonctions idiomatiques en Rocq tout en conservant les propriétés et théorèmes originaux. L'objectif est de faciliter l'interopérabilité entre ces deux environnements de preuve formelle pour des applications en vérification mathématique et en intelligence artificielle.

Bibliothèque dédiée à l'intégration de l'outil ZenonModulo avec Lambdapi pour générer des preuves formelles en logique. Elle facilite l'automatisation des démonstrations mathématiques et la vérification de théorèmes dans un cadre formel, en s'appuyant sur des outils de preuve automatisée existants.

HOL Light est un environnement interactif de démonstration et vérification de théorèmes mathématiques. Écrit en Objective CAML, il utilise le toplevel d'OCaml comme interface. Il est principalement utilisé pour la vérification formelle de preuves dans les domaines de la logique, de l'informatique théorique et des mathématiques.

GeoCoqInE-Euclid est un projet de démonstration de théorèmes géométriques automatisée, utilisant le langage de programmation fonctionnelle Coq et la bibliothèque Euclid. Il permet le développement et la vérification de preuves formelles, ainsi que le travail collaboratif sur des théories mathématiques.

Outil en ligne de commande conçu pour prouver des obligations de preuve au format POG en utilisant la plateforme Why3. Il permet de transformer des fichiers de preuve en formats compatibles avec divers prouveurs automatiques (Zenon, SMT-LIB, TPTP, etc.) pour valider des théorèmes mathématiques ou des propriétés logiques. Idéal pour les chercheurs et développeurs en vérification formelle ou en logique mathématique.

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 est la bibliothèque standard du Rocq Prover, un assistant de preuve interactif. Il propose un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, accompagnés d'un environnement pour développer des preuves vérifiées par machine. La bibliothèque standardise et organise les modules essentiels pour les utilisateurs et développeurs, favorisant ainsi la rigueur et la réutilisabilité dans les travaux de preuve formelle.

Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves formelles vérifiables par machine.

Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves vérifiées par ordinateur.