3 Résolution
Revenons à la règle de résolution. Rappelons que nous l'avons
énoncée comme suit :
- à partir des deux clauses C=G¾®D, A1,
..., Am et C'=A'1, ..., A'n,
G'¾®D', déduire les clauses Gs,
G's'¾® Ds, D's', pour toutes
substitutions s et s' qui rendent égaux exactement
A1s, ..., Ams à droite de C et
A'1s', ..., A'ns' à gauche de C'.
Comme le mgu est unique, nous savons que toutes les clauses résultat
Gs, G's'¾® Ds, D's'
sont en fait des instances d'une clause unique : Gs,
G'rs¾® Ds, D'rs, où
r renomme les variables libres de la seconde clause en de
nouvelles variables, non libres dans la première clause, et s
est le mgu de A1, ..., Am, A'1r, ...,
A'nr.
Ceci nous mène au principe de résolution, comme il est
réellement utilisé en recherche de preuve par résolution :
Définition 8 [Résolution]
La règle de résolution binaire est :
où nous supposons que les deux clauses G¾® D, A
et A',G'¾®D' sont renommées de sorte qu'elles
n'ont aucune variable libre en commun. La conclusion de la règle
est appelée le résolvant binaire des deux clauses, les
premisses sont appelées les clauses parentes, et A
(resp. ¬ A') est le littéral sur lequel on résout dans la
première clause (resp. second clause).
Nous disons que les littéraux A et ¬ A' sont complementaires à condition que A s'unifie avec A'.
La règle de factorisation est la règle double :
La conclusion de la règle est appelée un facteur binaire
de la clause en prémisse.
Un facteur d'une clause est soit la clause elle-même, soit
un facteur binaire d'un de ses facteurs. Un facteur propre
d'une clause est un facteur d'un de ses facteurs binaires.
Un résolvant de deux clauses est un résolvant binaire de
facteurs de chaque clause, non nécessairement propres.
Une dérivation par résolution est un arbre inversé
dont les noeuds sont étiquetés par des clauses, les feuilles
sont étiquetées par des clauses de l'ensemble initial de
clauses, et les noeuds internes ont comme prédécesseurs leurs
clauses parentes.
Une réfutation par résolution est une dérivation se
terminant sur la clause vide, autrement dit une dérivation dont la
racine est étiquetée par ¾®.
Remarquer que l'utilisation d'une règle séparée de factorisation
code des unifications multiples.
Théorème 9 [Correction, complétude]
Soit S0 une ensemble de clauses, et Sn la suite des
ensembles de clauses définie par Sn+1 égale l'ensemble de
tous les résolvants de clauses dans Sn (Sn est
appelé l'ensemble de niveau n).
Alors la résolution est une procédure de recherche de
réfutation correcte et complète, autrement dit,
l'ensemble S0, vu comme une conjonction universellement
quantifiée de clauses disjonctives, est insatisfiable si et
seulement s'il existe nÎN tel que Sn, nÎN
contienne la clause vide.
Preuve : La correction vient, comme dans le cas propositionnel, du fait que
la conjonction de deux clauses quelconques (ici, universellement
quantifiées) implique leurs résolvants.
La complétude est le fait que si S0 est insatisfiable, alors
il existe un ensemble de niveau qui contient la clause vide. Par
les observations de la section 1, si S0 est
insatisfiable, alors l'ensemble des instances closes de clauses dans
ÈnÎNSn contient la clause vide. (Ceci vient
de la complétude de la résolution propositionnelle et du
théorème de Herbrand.) Maintenant, la seule clause qui a la
clause vide comme instance est la clause vide elle-même. Donc la
clause vide est dans ÈnÎNSn, donc dans un des
Sn.
¤
On peut avoir l'impression que la factorisation est inutile, et que
les facteurs seront fabriqués par unification lors de la
résolution binaire. Ceci simplifierait en effet le codage de la
résolution. Malheureusement, les facteurs sont indispensables. Par
exemple, l'ensemble des deux clauses :
¾® P(x,a), P(a,x) |
P(y,a), P(a,y)¾® |
est insatisfiable, parce que ¾® P(a,a) est une facteur de la
première clause, P(a,a)¾® un facteur de la seconde, et la
clause vide en est un résolvant. Cependant, les seules clauses que
nous pouvons en extraire par résolution binaire uniquement sont
P(a,x)¾® P(a,x), P(y,a)¾® P(y,a) et P(a,a)¾®
P(a,a), mais pas la clause vide : la résolution binaire seule est
incomplète.
Voir [CL73] pour une autre preuve de la complétude de la
résolution. Chang et Lee procèdent par des arguments purement
sémantiques, en utilisant des arbres de Herbrand, que nous
avons déjà utilisés dans la preuve du théorème de Herbrand.