Hazel est un projet de formalisation Coq visant à vérifier des bibliothèques d'analyse numérique, telles que l'analyse définie par la règle et la différentiation automatique. Il définit un langage de programmation formel avec des effets et développe une logique de programmes pour raisonner sur les programmes qui peuvent effectuer des effets.

Ce projet propose une suite de benchmarks pour évaluer et comparer des outils de déduction automatique et de résolution de règles logiques. Il permet d'analyser les performances de solveurs comme InteGraal et OWLAPI dans des contextes de logique de règles, en fournissant des configurations standardisées et des fichiers de test reproductibles. Les résultats aident les chercheurs et développeurs à identifier les forces et faiblesses des différentes approches.

InteGraal est une plateforme open source dédiée à la gestion et au raisonnement sur des bases de connaissances exprimées en logique. Elle permet d'analyser, de manipuler et d'évaluer des règles logiques, des faits et des requêtes pour automatiser des processus de déduction et de vérification. Utilisée dans des contextes académiques et industriels, elle facilite l'intégration de moteurs de raisonnement dans des applications variées.

Ce projet est un moteur d'inférence conçu pour résoudre des problèmes complexes en appliquant des règles logiques et des faits prédéfinis. Il permet d'automatiser des raisonnements déductifs, d'analyser des données pour en tirer des conclusions, et d'aider à la prise de décision dans divers domaines comme l'intelligence artificielle ou l'aide à l'expertise.

NAKED est un outil dédié à l'analyse et à la visualisation de bases de connaissances basées sur des règles existentielles. Il permet de calculer les réparations logiques d'une base incohérente, de générer des hypergraphes d'argumentation et de représenter graphiquement ces structures de manière interactive. Utilisé principalement dans le domaine de la logique formelle et de l'intelligence artificielle, il facilite la compréhension des incohérences et des conflits au sein des données.

MajS est un outil dédié à l'analyse et à la comparaison de réseaux biologiques, notamment pour l'étude des voies de signalisation et des prédictions de nœuds biologiques. Il permet de générer des solutions optimales à partir de règles logiques appliquées à des instances biologiques, facilitant ainsi la validation et l'interprétation des modèles. Les résultats sont utilisés pour comparer les performances avec d'autres outils comme Iggy.