EQP, abréviation de equational prover (), est un programme automatisé de démonstration de théorèmes pour la logique équationnelle, développé par la Division de mathématiques et d'informatique du laboratoire national d'Argonne. C'est l'un des démonstrateurs utilisés pour résoudre un problème de longue date posé par Herbert Robbins, à savoir, si toutes les algèbres de Robbins sont des algèbres booléennes..
Notes et références
Voir aussi Article connexe Démonstration automatique de théorèmes
Liens externes Projet EQP Laboratoire national d'Argonne, Division des mathématiques et de l'informatique.
Catégorie:Assistant de preuve