Résumé : Il s'agit d'une implantation de l'algorithme de Stalmarck en ELAN en vue d'en faire une procedure de decision pour le compte du systeme de preuve COQ. l'algorithme de Stalmarck sert a tester la validite d'une formule propositionnelle. ELAN est un environnement pour specifier et prototyper des systemes de deduction, il se base sur le reecriture.