Cette thèse est dédiée au développement de langages de spécification formels, de leur sémantique opérationnelle sous forme de systèmes de réécriture décorés et des outils de preuves associés. Nous définissons les logiques Rn et Gn, qui sont des logiques à clauses de Horn égalitaires avec prédicat d'appartenance, adaptées à la spécification et à la programmation polymorphique d'ordre supérieur avec sous-typage dynamique et paramétrique, des fonctions strictes et partielles et une sémantique initiale basée sur la théorie des ensembles. Puis, nous introduisons les termes décorés, qui représentent une structure de données bien adaptées aux spécifications et programmes équationnels types. Ils permettent d'intégrer le raisonnement égalitaire, les fonctions partielles et le typage dynamique de termes