Ce projet fournit des encodages de règles d'inférence et de méta-théorèmes utilisés pour la vérification du prouveur automatique de théorèmes Leo-III en logique d'ordre supérieur. Les encodages sont développés dans le cadre du système Dedukti et exploités via l'assistant de preuve interactif Lambdapi. Il facilite la clausification, la simplification de termes et la gestion des littéraux pour les preuves automatisé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.