Dedukti est un vérificateur de types et un langage dédié à la formalisation et à la vérification de systèmes logiques et mathématiques. Il permet de définir des règles de réécriture et de vérifier leur cohérence, facilitant ainsi la construction de preuves formelles et la validation de propriétés dans des calculs avancés comme le lambda-calcul ou les systèmes de types dépendants.

Ce projet développe un système de preuve neuronale pour analyser et valider des structures linguistiques complexes en français. Il combine un super-tagger pour étiqueter les mots avec des catégories syntaxiques avancées et un linker pour établir les relations entre ces éléments. L'objectif est de transformer des phrases en représentations logiques structurées, facilitant ainsi l'analyse sémantique et la vérification automatique de cohérence grammaticale.

Outil permettant de parser et de vérifier la cohérence syntaxique et la bonne formation des scripts écrits dans le langage SMT-LIB version 2.6. Il facilite l'analyse de fichiers contenant des logiques, des théories ou des commandes de vérification, en s'appuyant sur des théories et logiques prédéfinies pour valider la structure des termes et des assertions.

Outil dédié à la résolution de problèmes de satisfaction de contraintes (CSP) et à la validation de propriétés logiques sur des modèles formels. Il permet d'analyser des systèmes critiques en vérifiant leur cohérence et en générant des contre-exemples ou des preuves de validité. Développé dans le cadre d'un projet de recherche financé par l'ANR, il s'appuie sur des techniques avancées de logique et de satisfiabilité.