Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories equationnelles / Claude Marché ; sous la dir. de Jean-Pierre Jouannaud

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 1993

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Knuth -- Donald Ervin -- 1938-....

Réécriture, Systèmes de (informatique)

Décidabilité (logique mathématique)

Classification Dewey : 511.3

Jouannaud, Jean-Pierre (Directeur de thèse / thesis advisor)

Université Paris-Sud (1970-2019) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : 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 equationnelle. 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 base 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 s-normalisée pour plusieurs classes intéressantes de théories s-closes. Nous obtenons alors des résultats de décidabilité du problème du mot pour certaines classes de théories equationnelles, incluant le cas ac-clos (déjà obtenu par Narendran et Rusinowitch), le cas ac1i-clos (un nouveau résultat), et le cas des théories closes modulo les théories des groupes abéliens et des anneaux commutatifs, qui est déjà connu dans le cas où la signature contient uniquement des constantes (Kandri-Rody et Kapur), 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. Enfin, nous avons implanté la complétion normalisée et montré ainsi son efficacité en pratique par rapport à la complétion modulo ac