Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certains classes de théories équationnelles

Résumé

Nous définissons une nouvelle relation de réécriture sur les termes, la réécriture normalisée, qui étend la notion déjà connue de réécriture modulo une théorie équationnelle. Cette nouvelle relation de réécriture permet de travailler modulo des théories pour lesquelles la notion précédente ne pouvait pas s'appliquer, en particulier pour les cas des axiomes d'élément neutre, d'idempotence, des groupes abéliens et des anneaux commutatifs. Nous décrivons un algorithme de complétion basé sur la réécriture normalisée qui contient comme instance la complétion de Knuth et Bendix, mais aussi des algorithmes de calcul de bases standard d'idéaux de polynômes, de Buchberger et de Kandri-Rody et Kapur.

Nous nous intéressons ensuite au cas particulier de la complétion d'équations closes, et nous montrons par une méthode uniforme la terminaison du processus de complétion E-normalisée pour plusieurs classes intéressantes de théories E-closes, ce qui généralise à la fois le résultat de Narendran et Rusinowitch pour le cas AC-clos et le résultat de Buchberger et celui de Kandri-Rody et Kapur pour les idéaux de polynômes.

Nous obtenons alors des résultats de décidabilité du problème du mot pour certaines classes de théories équationnelles, incluant le cas AC-clos, le cas AC1I-clos (un nouveau résultat à notre connaissance), et le cas des théories closes modulo les theóries des groupes abéliens et des anneaux commutatifs, qui est déjà connu dans le cas où la signature contient uniquement des constantes, mais qui est nouveau dans le cas général.

Nous avons également montré un résultat d'indécidabilité du problème du mot dans un cas intermédiaire entre AC et les anneaux, le cas ACD-clos, un résultat également nouveau à notre connaissance.

Enfin, nous avons implanté la complétion normalisée et montré ainsi son efficacité en pratique par rapport à la complétion modulo AC.

abstract
version complête