Idées fondamentales

1 Idées fondamentales

L'idée principale est due à J. Alan Robinson en 1965. Il y a deux ingrédients dans la méthode de résolution : la résolution propositionnelle, que nous avons déjà examinée, et l'unification, qui la rend utilisable lorsqu'on transpose la méthode au premier ordre.

Considérons une formule F du premier ordre, dont nous voulons savoir si elle est valide. Comme en résolution propositionnelle, nous la nions, et essayons d'en dériver une contradiction. Pour ce faire, nous skolémisons ¬F (rappelons que la forme de Skolem est insatisfiable si et seulement si ¬F l'est), et obtenons une formule de la forme " x₁· ... " x_n·Y. Nous pouvons maintenant écrire Y en forme clausale, comme dans le cas propositionnel : Y est la conjonction de clauses C₁, ..., C_m. Alors, par la construction de Herbrand, ¬F est insatisfiable si et seulement si la conjonction d'un nombre fini d'instances closes des clauses C_i, 1£ i£ m, est insatisfiable, c'est-à-dire propositionnellement insatisfiable, puisqu'il ne reste aucun quantificateur.

(where A=A₁s=...=A_ms=A'₁s'=...=A'_ns')

Figure 1: Relèvement

Ensuite, nous pouvons utiliser la résolution propositionnelle. En particulier, F est valide si et seulement s'il existe un ensemble fini S d'instances closes des clauses C_i tel que l'on peut dériver la clause vide ¾® à partir de S en n'utilisant que la règle Cut.

La vraie invention de Robinson a été de concevoir l'unification pour factoriser tous les aspects communs entre toutes les applications de Cut sur des instances closes différentes des mêmes clauses. Regarder la figure 1, où on a représenté deux clauses C= G¾®D, A₁, ..., A_m et C'=A'₁, ..., A'_n, G'¾®D', d'instances closes respectives Gs ¾® Ds, A et A, G's'¾® D's', où A= A₁s= ...= A_ms= A'₁s'= ...= A'_ns'. Par la règle Cut propositionnelle, ces deux dernières clauses produisent la clause close Gs, G's' ¾® Ds, D's'.

Maintenant supposons que A₁, ..., A_m soient les seuls atomes à droite de C tels que A_is=A, et que A'₁, ..., A'_n soient les seuls atomes à gauche tels que A'_is'=A. Toute coupure propositionnelle entre les clauses closes Cs et C's a la même structure que ci-dessus, quelles que soient les valeurs de s et s', du moment qu'elles identifient toutes A₁s, ..., A_ms à droite de C et A'₁s', ..., A'_ns' à gauche de C'. Nous pouvons regrouper toutes ces déductions en une règle unique, la règle de résolution :

à partir des deux clauses C=G¾®D, A₁, ..., A_m et C'=A'₁, ..., A'_n, G'¾®D', déduire les clauses Gs, G's'¾® Ds, D's', pour toutes substitutions s et s' qui rendent égaux exactement A₁s, ..., A_ms à droite de C et A'₁s', ..., A'_ns' à gauche de C'.

Ceci ne semble pas meilleur que l'énumération de toutes les instances closes des clauses, suivie de la coupure. C'est en fait bien meilleur, parce que le processus d'unification, que nous rappelons en section 2, donne une représentation concise de l'ensemble des substitutions possibles s et s', comme l'ensemble des instances d'une substitution unique, appelée l'unificateur le plus général de A₁, ..., A_m, et de versions renommées de A'₁, ..., A'_n.