Lambdapi est un assistant de preuve basé sur le λΠ-calcul modulo réécriture, offrant des interfaces utilisateur pour Emacs et VSCode. Il permet de certifier des preuves pour différents systèmes de preuve, tels que TLAPS, Atelier B, Rodin, LISA, et Why3.

Logipedia is a project that aims to translate and share formal proofs between several systems. The website displaying all available proofs can be reached at http://logipedia.science.

Agda2Dedukti est un traducteur permettant de convertir des preuves formelles écrites dans le langage Agda vers les langages Dedukti et Lambdapi, facilitant ainsi la vérification de ces preuves.

Zenon Modulo est un solveur de preuves automatisé pour la logique du premier ordre classique avec types polymorphes. Il accepte les fichiers d'entrée avec la syntaxe TPTP (FOF et TFF1) et Dedukti. Il peut produire des certificats de preuve pour Dedukti. Il est utilisé dans les projets FoCaLiZe et BWare.

CoqInE est un plugin pour le logiciel Coq qui traduit les preuves Coq en termes Dedukti vérifiables. Il fournit un fichier de signature fidèlement encodant la théorie sous-jacente de Coq. La sortie générée est destinée à être vérifiable à l'aide de la dernière version de Dedukti.

The lean2dk project is a translation tool that converts formal proofs from the Lean proof assistant to the Dedukti system, facilitating the exchange of formal proofs between different systems and promoting the use of formal methods in mathematics and computer science.

Ce programme vérifie la terminaison d'autres programmes en utilisant le critère de terminaison Size-Change. Il accepte en entrée des fichiers Dedukti ou des fichiers XML de la Termination Problem Data Base.

Le projet coq-hol-light est une bibliothèque Coq contenant une traduction automatique de la bibliothèque HOL-Light, utilisant hol2dk et lambdapi. Cette bibliothèque fournit des axiomes pour les théorèmes traduits, permettant une vérification rapide dans Coq. Elle vise à fournir une bibliothèque directement utilisable dans Coq, alignant les fonctions et prédicats HOL-Light sur ceux définis dans la bibliothèque standard Coq.

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.

La bibliothèque Lambdapi est une implémentation en logique intuitionniste du premier ordre de types de données tels que les ensembles, la logique propositionnelle, l'égalité de Leibniz, la logique du premier ordre, les booléens et les nombres naturels, ainsi que des listes polymorphiques.