Abstract FR:

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 refutationnelle 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 rencontre. 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.