Abstract FR:

L'objet de cette thèse est la réalisation d'un outil de preuve pour la terminaison des systèmes de réécriture équationnels. Tout particulièrement dans le cas de la théorie associative-commutative. Nous fondant sur un théorème général de terminaison équationnelle, nous construisons un ordre sur les termes, possédant les propriétés requises par ce théorème. Puis nous donnons les justifications théoriques des propriétés de notre ordre, apportant ainsi un outil validé de preuve de terminaison des systèmes de réécriture associatifs-commutatifs. Nous proposons de plus une démonstration complète d'une propriété de l'ordre qui rend cette méthode de preuve implantable dans le cas général des termes avec variables : La stabilité par instanciation. Nous exposons enfin le champ d'application de l'ordre construit, en expliquant son fonctionnement sur une série d'exemples usuels de systèmes de réécriture associatifs-commutatifs