Notre objectif dans cette thèse est de vérifier la validité d'une formule équationnelle dans une spécification algébrique axiomatisée par un ensemble d'équations. Une formule équationnelle est une formule universellement quantifiée d'un langage du premier ordre dont les formules atomiques sont des équations simples. Nous proposons de généraliser et d'adapter les méthodes utilisées dans le cas des équations simples pour prouver la validité des formules équationnelles. Ainsi, dans le cas de la validité inductive nous avons utilisé l'induction structurelle basée sur la récurrence classique. Nous avons proposé une méthode pour la génération automatique des schémas d'induction dans certains cas particuliers. Dans le cas de la validité équationnelle nous avons proposé une méthode basée sur la transformation et la décomposition de la formule initiale pour déterminer un ensemble représentatif d'équations simples. La validité équationnelle de ces équations est équivalente à celle de la formule initiale. Un autre mécanisme de raisonnement appelé le chaînage transitif est proposé pour tester la validité des équations contenant des relations d'ordre. L'étude théorique des principes proposés dans cette thèse a abouti à la réalisation du système de preuve pause que nous avons utilisé pour vérifier certaines relations d'asynchronisme entre les composantes qui gèrent la communication dans un système parallèle