Déduction automatique avec contraintes
symboliques dans les théories équationnelles
Doctorat de l'Université Henri
Poincaré
obtenu le 18 novembre 1994 avec la mention
Très Honorable
par Laurent Vigneron
Directeur de thèse :
Laboratoire d'accueil :
Laboratoire lorrain de recherche en informatique et ses applications
(LORIA).
[ nommé CRIN à l'époque ]
Campus Scientifique, B.P. 239 -
54506 Vandoeuvre-lès-Nancy Cedex.
Laboratoire associé
au C.N.R.S. et à
l'INRIA - UMR 7503
Équipes d'accueil :
EURECA
(jusqu'à janvier 1993), équipe dirigée par Pierre Lescanne, Directeur
de Recherche au C.N.R.S, puis PROTHEO,
équipe dirigée par Claude Kirchner, Directeur
de Recherche à l'INRIA.
Rapporteurs :
Philippe Jorrand, Directeur de Recherche au C.N.R.S,
René Schott, Professeur à l'Université Henri
Poincaré,
Wayne Snyder, Professeur à l'Université de Boston.
Membres du jury :
Jean-Pierre Jouannaud
(Président), Professeur à
l'Université de Paris-Sud,
Ricardo Caferra,
Maître de Conférences à
l'ENSIMAG,
Hélène
Kirchner, Chargée de Recherche au C.N.R.S,
Michaël Rusinowitch,
Directeur de Recherche à l'INRIA,
René Schott, Professeur
à l'Université Henri Poincaré,
Wayne Snyder,
Professeur à l'Université de Boston.
Résumé de la thèse :
Nous proposons dans ce document des techniques de déduction
automatique pour effectuer des preuves de propriétés
par réfutation dans la logique du premier ordre. Ces preuves
sont réalisées modulo un ensemble d'axiomes formant
une théorie régulière E.
Les systèmes d'inférence définis sont
fondés sur les règles de résolution et de
paramodulation. Nous proposons plusieurs stratégies de
sélection de clauses (ordonnée ou positive), et de
remplacement (paramodulation ou superposition). Nos règles
d'inférence évitent la combinatoire de l'usage des
axiomes de E, par un calcul de contextes de
remplacements et un algorithme d'unification modulo E. En
plus de ces règles d'inférence, nous
définissons des règles de simplification permettant
d'éliminer les clauses redondantes. Nous démontrons la
complétude réfutationnelle de ces systèmes
grâce à une extension de la technique des arbres
sémantiques transfinis.
Pour le cas des théories associatives et commutatives, nous
montrons que l'on peut éviter de résoudre les
problèmes d'unification. Seul le test d'existence d'une
solution est nécessaire. Ainsi, tout problème
d'unification est ajouté à la clause déduite
sous la forme d'une contrainte, de même que toute autre
condition non résolue pour appliquer l'inférence.
Cette stratégie contrainte simule la stratégie basique
et n'engendre qu'une seule clause par étape
d'inférence, au lieu d'autant de clauses que de solutions au
problème d'unification rencontré.
Nous décrivons le logiciel daTac, implantant les
résultats présentés dans ce document, pour le
cas des théories associatives et commutatives.
Mots clés :
Déduction automatique, théorie équationnelle,
résolution, paramodulation, réécriture,
contraintes symboliques, stratégie basique, arbres
sémantiques.
Si vous voulez récupérer la thèse, cliquez sur
[Thèse].
