Le but de cette thèse est de proposer de nouveaux outils pour la déduction automatique dans les théories associative-commutatives. Dans le cadre de la réécriture, nous proposons une nouvelle définition de la réécriture modulo ac en restreignant la réécriture de Peterson et Stickel à certaines positions appelées positions utiles modulo ac. Ceci permet de réduire d'une part le nombre de paires critiques à calculer lors de la complétion d'un système de réécriture. Dans le domaine de l'unification, nous proposons tout d'abord un nouvel algorithme de résolution des systèmes d'équations diophantiennes linéaires qui interviennent dans l'unification modulo ac, ainsi qu'une formule permettant un dénombrement rapide des solutions minimales d'un problème d'unification modulo ac. Cela permet de développer des stratégies pour tous les processus dans lesquels on est amène à faire un choix sur le problème à résoudre, comme par exemple le calcul de paires critiques lors de la complétion d'un système de réécriture, ou encore la résolution paresseuse de contraintes en logique équationnelle contrainte. Enfin, nous proposons une méthode permettant, pour toute spécification dont la présentation contient les axiomes d'associativité et de commutativité, d'en construire une extension conservative modulo laquelle l'unification devient moins complexe en termes de nombre de solutions minimales. Les solutions d'un problème d'unification modulo la nouvelle spécification peuvent alors vues comme des schémas représentent chacun un grand nombre des solutions modulo la spécification de départ