Abstract FR:

La premiere partie de cette these traite d'ordres sur les termes. Nous montrons d'abord que l'ordre recursif sur les chemins avec ensemble inevitable de motifs ne permet pas de montrer la terminaison de tous les systemes de reecriture noetheriens. Nous etudions ensuite des ordres permettant de comparer des termes dans les theories associatives-commutatives. Nous etendons l'ordre apo introduit par bachmair et plaisted, au cas d'une chaine de symboles associatifs commutatifs et au cas d'une chaine de symboles unaires compris entre deux symboles associatifs-commutatifs. Dans une deuxieme partie, nous nous interessons a la transformation de problemes equationnels. Nous montrons d'abord la confluence d'un systeme permettant de transformer des formules en problemes d'unification. Puis nous prouvons la terminaison d'un systeme transformant les formules equationnelles dans les algebres de sortes ordonnees. Cette derniere partie a ete effectuee en collaboration avec h. Comon