Optimisations

4 Optimisations

La résolution est assez inefficace au niveau propositionnel. Si nous séparons la résolution au premier ordre en ses deux composantes, la résolution propositionnelle et le relèvement au premier ordre par unification, alors seule la première composante reste à améliorer. Heureusement, on peut raffiner la résolution de nombreuses façons pour la rendre plus efficace. Certaines des idées viennent de la procédure de Davis-Putnam, d'autres tentent de restreindre les dérivations par résolution à des dérivations presque canoniques pour éviter les redondances.

4.1 Stratégies de sélection de clauses

La première chose que nous devons examiner est le processus de sélection des clauses. Le seul que nous avons présenté pour l'instant, la recherche par saturation de niveaux, est complète, mais produit de nombreuses clauses inutiles.

Nous diminuerons fortement les chances de tomber sur les configurations les pires en utilisant diverses optimisations, voir les sections 4.2 ou 4.4. Il nous faudra y adjoindre des stratégies plus fines d'exploration de l'espace des dérivations par résolution.

La recherche par saturation de niveaux produit toutes les dérivations possibles en parallèle. D'abord toutes les dérivations de profondeur 1, qui fabriquent les clauses de S₁, ensuite les dérivations de profondeur 2, qui fabriquent les clauses de S₂, et ainsi de suite. Mais l'on n'est pas obligé de suivre une telle stratégie. En fait, tout ce que nous voulons, c'est explorer l'espace de toutes les dérivations de sorte qu'aucune étape de résolution ne soit remise à plus tard indéfiniment longtemps. Il s'agit d'une condition d'équité (``fairness'' en anglais) :

Définition 10 [Équité] Une stratégie de sélection de clauses est dite équitable si et seulement s'il n'existe pas de paire de clauses ignorées infiniment longtemps par la stratégie. (De façon équivalente, si l'ensemble des résolvants produits par la stratégie est exactement l'union de tous les ensembles de niveaux.)

Il est alors clair que n'importe quelle stratégie équitable, et pas seulement la recherche par saturation de niveaux, préserve la complétude de la résolution. La recherche par saturation de niveaux est coûteuse en termes tant d'espace que de temps. La recherche en profondeur d'abord utilise la mémoire à meilleur escient : choisir une paire de clauses, résoudre, ajouter le résolvant à l'ensemble des clauses, et continuer; ensuite, rebrousser chemin (``backtrack'' en anglais) et choisir une autre paire de clauses à résoudre si l'on réalise plus tard que cette paire ne mène pas à une réfutation. Le nombre de clauses engendrées que nous devons garder en mémoire au niveau k est alors O(k), c'est-à-dire bien moins que dans la recherche par saturation de niveaux, où on doit en garder une exponentielle en k.

Le problème est que la recherche en profondeur d'abord n'est pas équitable. Mais on peut y remédier en utilisant l'astuce suivante, appelée approfondissement itéré (``iterative deepening'' en anglais) : on se fixe une limite kÎN, puis on effectue une recherche en profondeur comme ci-dessus, mais on rebrousse chemin si la clause vide n'a pas été produite en moins de k étapes de résolution; si aucune réfutation n'a pu être obtenue en moins de k étapes de résolution, nous le découvrirons en temps fini; si c'est la cas, augmenter k et recommencer. Ce faisant, nous reproduirons tous les calculs que nous avons déjà effectués, fabriquant des résolvants à des niveaux plus petits que l'ancienne valeur de k, mais ceci prend usuellement moins de temps que l'exploration de tous les nouveaux résolvants au niveau k+1. (Par exemple, supposons que nous passions un temps O(2^k) pour explorer les clauses dans S_k, alors pour explorer celles de S_k+1, nous y passerons un temps O(2^k+1), dont seule la moitié est consacrée à la réexploration d'anciennes clauses.)

Nous allons maintenant chercher à réduire l'ensemble des clauses qui valent la peine d'être produites. Ceci réduira l'espace des dérivations par résolution qui nous intéresseront, mais pas suffisamment pour que cet espace devienne fini. Dans tous les cas, nous aurons besoin de stratégies équitables de sélection de clauses.

4.2 Stratégies d'effacement

Les stratégies d'effacament (``deletion strategies'' en anglais) éliminent des clauses inutiles qui, si on les conservait, pollueraient le processus de recherche de preuve en augmentant artificiellement la taille de l'ensemble de clauses.

4.2.1 Élimination des clauses subsumées

Définition 11  [Subsomption]  Soit C = G¾® D et C' une autre clause. Nous disons que C subsume C', et nous notons C³ C', si et seulement si C' est de la forme G', Gs ¾® Ds, D' pour une certaine substitution s.

Autrement dit, C subsume toutes les clauses obtenues en affaiblissant une de ses instances. Considérons C et C' comme des disjonctions universellement quantifiées de littéraux : sémantiquement, si C subsume C', alors C implique C'.

Les clauses subsumées sont normalement inutiles, à cause de :

Lemme 12   Soient C₁ et C'₁ deux clauses telles que C₁ subsume C'₁. Pour tout résolvant C' entre C'₁ et C₂, C' est subsumée par C₁ ou par un résolvant de C₁ et C₂.

De plus, l'unique clause qui subsume la clause vide est la clause vide.
Preuve : Notons C₁ G₁¾® D₁, et C'₁ G'₁, G₁s₁ ¾® D₁s₁, D'₁. Si C' est un facteur de C'₁, il est clairement subsumé par C₁. Nous vérifions maintenant le lemme sur les résolvants binaires. Supposons que nous ayons obtenu C' par résolution binaire sur un atome A'₁ à droite de C'₁ et un atome A₂ à gauche de C₂. (Le cas symétrique est similaire.)

Premier cas : A'₁ÎD'₁. Soit D''₁= D'₁\ {A'₁}, C₂ = A₂, G₂¾® D₂, et s' = mgu(A'₁,A₂). Alors C'₁= G'₁, G₁s₁ ¾® D₁s₁, D''₁, A'₁, C'= G₂s', G'₁s', G₁s₁s' ¾® D₁s₁s', D''₁s', D₂s'. Donc C'£ C₁.

Second cas : A'₁Î D₁ s₁. Soit A'₁ égale A''₁ s₁, D''₁= D₁ \ {A''₁}, C₂ = A₂, G₂ ¾® D₂, et s' = mgu(A''₁ s₁, A₂). Comme A''₁ s₁ s'= A₂ s', et comme fv(A''₁) Ç fv(A₂)= Ø, la substitution s₁ s' È s' est un unificateur de A''₁ et A₂, disons sq, où s= mgu(A''₁, A₂). Alors nous pouvons résoudre C₁ avec C₂, sur A''₁ et A₂ respectivement, ce qui produit C = G₁ s, G₂ s ¾® D''₁s, D₂s. Puisque C'= G₂ s q, G'₁ s q, G₁ s q ¾® D''₁ s q, D'₁ s q, D₂ s q, C subsume C'.

Finalement, si G¾®D subsume la clause vide, alors G et D doivent être vides, autrement dit seule la clause vide subsume la clause vide. ¤

Corollaire 13   Soit S et S' deux ensembles de clauses. Supposons que toute clause C de S est dans S' ou est subsumée par une clause de S'.

Si la clause vide est dérivable à partir de S en k étapes de résolution, alors elle est dérivable à partir de S' en au plus k étapes de résolution.
Preuve : Par récurrence sur k. Si k=0, alors la clause vide est dans S, donc par hypothèse elle est dans S' ou elle est subsumée par une clause de S'; dans chaque cas, la clause vide doit déjà être dans S'. Sinon, supposons que le résultat soit valide pour k-1 étapes, et que nous puissions dériver la clause vide de S en k étapes, k>0. Examinons la première étape de résolution dans la dérivation : nous résolvons deux clauses C₁ et C₂ pour produire le résolvant C.

Par hypothèse, C₁ est subsumée par une clause C'₁ de S' (éventuellement C₁ elle-même), et C₂ est subsumée par une clause C'₂ de S'. Par le lemme 12, C est subsumée par une clause C', qui peut être C'₁, C'₂ ou un résolvant de C'₁ et C'₂. Alors, SÈ{C} et S'È{C'} sont deux ensembles de clauses vérifiant les conditions du théorème, et nous pouvons dériver la clause vide en k-1 étapes de SÈ{C}. Par hypothèse de récurrence, nous pouvons dériver la clause vide en au plus k-1 étapes de S'È{C'}, donc en au plus k étapes de S'. ¤

Nous pouvons donc éliminer les clauses subsumées comme suit. Si S est l'ensemble courant de clauses, nous enlevons de S toute clause subsumée par une autre clause de S tant que c'est possible. Ceci fournit un ensemble minimal S' comme dans le corollaire. Puis nous produisons un nouveau résolvant, et effaçons les clauses subsumées de l'ensemble résultant, et ainsi de suite. C'est complet parce que si nous sommes à une distance de k résolvants de la clause vide, le fait d'effacer des clauses subsumées nous laisse à au plus k résolvants de la clause vide, et si nous calculons le bon résolvant, nous serons alors à au plus k-1 résolvants de la clause vide, et ainsi de suite.

Une façon erronée d'effacer des clauses subsumées est de repérer toutes les clauses subsumées dans S et de les effacer en masse. En effet, le préordre de subsomption peut avoir des cycles lorsque différentes versions renommées de la même clause sont présentes dans S. Considérons l'exemple suivant : S={¾® P(x), ¾® P(x'), P(y)¾®}. S est insatisfiable, mais les deux premières clauses se subsument l'une l'autre; alors que {¾® P(x'), P(y)¾®} et {¾® P(x), P(y)¾®} sont tous les deux des sous-ensembles insatisfiables de S (des sous-ensembles S' comme dans le corollaire 13), l'élimination de toutes les clauses subsumées de S ne nous laisse que la clause P(y)¾®, qui est satisfiable.

On utilise la subsomption essentiellement de deux façons. La subsomption avant (``forward subsumption'') consiste en : chaque fois que nous fabriquons des résolvants à partir de clauses dans l'ensemble courant S, nous ne gardons que les résolvants qui ne sont pas subsumés par aucune clause de S. D'un autre côté, la subsomption arrière (``backward subsumption'') consiste à faire que quand nous produisons des résolvants C à partir de clauses dans l'ensemble courant S, nous effaçons de S toutes les clauses subsumées par C. On peut utiliser une combinaison des deux, par exemple la subsomption avant, puis arrière si le résolvant a survécu à la subsomption avant.

Remarquons aussi que la subsomption avant ne doit être utilisée que sur les résolvants, pas sur toutes les clauses, et en particulier pas sur les facteurs. En effet, un facteur d'une clause C est toujours subsumé par C : si la subsomption avant sur les facteurs préservait la complétude, alors on n'aurait pas besoin de la factorisation pour assurer la complétude de la méthode.

Calculer si une clause C est subsumée par une autre clause C' est difficile. En fait, le problème est NP-complet. En effet, bien que déterminer si un atome B est de la forme As soit facile (c'est du filtrage (``matching''), et ça peut se tester en temps polynomial par une modification simple de l'algorithme d'unification, où le test d'occurrence n'est plus nécessaire), au contraire pour décider la subsomption, nous devons d'abord deviner, ou trouver en rebroussant éventuellement chemin, une fonction des littéraux A' de C' vers le littéraux A de C, telle que A=A's pour une certaine substitution commune s. On peut améliorer cette procédure en remarquant que A' ne peut s'instancier en A que s'ils ont le même symbole de prédicat au sommet, de sorte que nous n'avons besoin d'explorer que les atomes A qui ont le même symbole de prédicat que A', pour tout A'. On peut encore faire mieux en considérant les symboles de fonction apparaissant aux diverses positions dans chaque atome, mais c'est plus compliqué, et nous ne le décrirons pas ici.

En pratique, le problème est encore plus difficile parce que ce qui nous intéresse n'est pas de savoir si C est subsumée par une clause donnée C', mais par une clause inconnue dans l'ensemble, éventuellement très grand, de clauses S. Il existe des méthodes efficaces pour résoudre ce problème, qui fonctionnent en général très rapidement. Mentionnons une solution, analogue aux réseaux de discrimination (``discrimination nets'') du prouveur Otter de Larry Wos, et utilisée par Andrei Voronkov dans son prouveur Vampire. On compile chaque atome, puis chaque clause, sous forme d'une suite d'instructions d'une machine abstraite (qui a des instructions qui empilent et dépilent des termes sur une pile, qui testent l'égalité de termes, qui lient des variables à des termes, et ainsi de suite), dont le rôle est de tester si un atome ou une clause donné subsume un atome ou une clause donné en argument. Comme ces programmes sont des chaînes de byte-codes, on peut les partager via leurs préfixes communs, en en créant des noeuds de choix, ce qui fait de l'ensemble de programmes un arbre. Le partage des préfixes de ces programmes fait que le programme arborescent qui en résulte effectue les tests de subsomption sur de nombreuses clauses en parallèle en général [Vor94].

4.2.2 Élimination de tautologies

La stratégie d'effacement la plus simple est l'élimination de tautologies. Une clause tautologique est une clause de la forme G,A¾® A,D pour un certain atome A. (Si nous voyons les clauses comme des disjonctions atomiques, avoir à la fois A et ¬ A est en effet la seule façon d'en faire une tautologie.) Éliminer les tautologies signifie que chaque fois que nous produisons un résolvant, nous ne l'ajoutons à l'ensemble courant de clauses que s'il n'est pas une tautologie (et qu'il n'est pas subsumé par les clauses précédentes).

Intuitivement, les tautologies n'apportent rien à la découverte d'une preuve, parce qu'elles sont toujours vraies. Ce n'est pas une justification, cependant. Mais l'élimination des tautologies est justifiée par :

Lemme 14 Soit C une clause tautologique. Alors tout résolvant de C avec n'importe quelle clause C' est une tautologie ou est subsumée par C'.
Preuve : Tout facteur de C' est subsumé par C. Nous examinons le cas des résolvants binaires entre C et C'. Soit C égale A, G¾® D, A. Si nous ne résolvons pas sur A, alors le résultat est encore une tautologie. Sinon, posons C' égale A, G'¾®D' (le cas symétrique est similaire), alors le résolvant est A, G, G' ¾® D', D, qui est subsumé par C. ¤

De plus, aucune tautologie ne peut être la clause vide. Donc la génération de nouvelles tautologies est inutile, ainsi que celle des clauses subsumées.

L'élimination des tautologies en résolution au premier ordre est similaire à l'élimination de tautologies dans la méthode de Davis-Putnam.

4.2.3 Élimination de clauses pures

Une autre simplification que nous pouvons adapter de la méthode de Davis-Putnam au cas de la résolution au premier ordre est l'élimination des clauses pures.

Définition 15 Soit S un ensemble de clauses.

Une clause C est dite pure dans S si et seulement si elle contient un littéral pur, autrement dit elle est de la forme G ¾® D, A, (resp. A, G ¾® D) où A ne s'unifie avec aucun atome à gauche (resp. à droite) d'aucune clause dans S. Si c'est le cas, nous disons que A (resp. ¬ A) est un littéral pur dans la clause C.

Nous pouvons toujours éliminer les clauses pures, qu'elles viennent d'être produites ou qu'elles soient déjà présentes dans l'ensemble courant de clauses S, parce que :

Lemme 16 Tout résolvant d'une clause pure avec n'importe quelle clause est pure.
Preuve : Tout facteur d'une clause pure est clairement encore pure. Ensuite, toute résolution binaire entre une clause où A (resp. ¬ A) est pur avec une autre clause doit opérer sur un autre littéral B. Le résolvant binaire produit doit donc contenir le littéral A (resp. ¬ A), et est donc pur. ¤

Comme aucune clause pure ne peut être vide, nous concluons que les clauses pures représentent des impasses dans la recherche de la clause vide. Nous pouvons donc éliminer les clauses pures sans sacrifier la complétude.

En fait, nous pouvons combiner toutes les stratégies d'effacement que nous avons mentionnées (la subsomption, l'élimination de tautologies, l'élimination de clauses pures) tout en conservant la complétude de la résolution. Regardons maintenant ce que nous avons au niveau propositionnel (où la factorisation n'est pas nécessaire) : la résolution binaire est similaire à une étape de la règle de séparation (``splitting'') de Davis et Putnam (si l'on fait toutes les résolutions possibles sur un atome donné A, on produit en fait toutes les clauses de la règle de séparation --- nous éclaircirons ce point en section 4.3); l'élimination de tautologies, resp. de littéraux purs, correspondent directement aux opérations des mêmes noms dans la méthode de Davis-Putnam. Les seules différences sont : en résolution propositionnelle, la subsomption avant revient à ne pas fabriquer d'affaiblissements de clauses précédentes, ce qui généralise la mémoïsation des clauses précédemment engendrées dont nous avions besoin pour faire terminer la résolution propositionnelle; le fait de produire des résolvants est en général moins efficace que d'utiliser la règle de séparation de la méthode de Davis-Putnam; et nous n'avons pas l'équivalent de la règle des clauses unitaires en résolution.

4.2.4 Résolution unitaire

Pour faire un parallèle avec la règle des clauses unitaires de la procédure de Davis-Putnam procedure, définissons un cas particulier de la règle de résolution, la résolution unitaire :

Définition 17 Une clause unitaire est une clause de la forme ¾® A ou A¾®, où A est un atome.

La résolution unitaire est la variante de la résolution où la résolution binaire est contrainte de sorte qu'au moins une des clauses parentes soit unitaire.

En d'autres termes, dans la résolution unitaire, pour appliquer la résolution binaire sur des clauses non unitaires, nous devons d'abord factoriser au moins une des clauses pour en faire une clause unitaire.

Malheureusement, la résolution unitaire n'est pas complète. Par exemple, l'ensemble de clauses propositionnelles :

¾® A,B

A¾® B

A,B¾®

B¾® A

est insatisfiable, mais on ne peut pas le montrer en n'utilisant que la résolution unitaire, parce qu'il ne contient pas de clause unitaire.

La résolution unitaire demande bien plus que l'application de la règle des clauses unitaires dans la méthode de Davis-Putnam : cette dernière règle était appliquée dès que possible, mais pas à l'exclusion des autres règles. Nous pourrions donc vouloir assouplir la contrainte sur la résolution unitaire comme suit : utiliser la résolution unitaire dès que possible, sinon utiliser la résolution générale. Mais ceci aussi est incomplet, autrement dit cette stratégie n'est pas équitable : considérons l'ensemble des clauses ci-dessus, plus :

¾® P(a)

P(x) ¾® P(f(x))

L'ensemble total est encore insatisfiable, mais on pourra appliquer la résolution unitaire indéfiniment, et on n'obtiendra que des clauses de la forme ¾® P(f^k(a)), k³ 1, mais jamais la clause vide.

Un cas particulier important est cependant :

Définition 18 [Horn] Une clause de Horn est une clause qui a au plus un atome sur le côté droit (c'est-à-dire un séquent intuitionniste atomique).

Un ensemble de Horn est un ensemble de clauses de Horn.

Lemme 19 La résolution unitaire est complète pour les ensembles de Horn.
Preuve : Exercice. (Le montrer d'abord dans le cas propositionnel; observer que la règle d'élimination de clauses unitaires par la méthode de Davis-Putnam est complète à elle seule dans le cas présent, et traduire toute dérivation de la clause vide ainsi obtenue en une preuve par résolution unitaire.) ¤

4.3 Stratégies ordonnées

Dans la méthode de Davis-Putnam, la séparation élimine un atome A en réécrivant l'ensemble S de clauses en deux ensembles S[T/A] et S[F/A], où A n'apparaît plus. Ce processus élimine les atomes un à un, jusqu'à ce qu'il n'en reste plus. La règle de résolution élimine aussi un atome, mais seulement entre deux clauses. Un problème majeur, alors, est la nature hautement non déterministe de ce processus d'élimination.

Considérons pas exemple les quatre clauses :

¾® A,B

A¾® B

B¾® A

A,B¾®

Nous pouvons choisir de résoudre la plupart des paires de clauses soit sur A soit sur B. Si nous choisissons de résoudre sur A, les seuls choix qui ne produisent pas de tautologies sont entre la première et la deuxième clause, ce qui donne ¾® B, ou entre la troisième et la quatrième, ce qui donne B¾®. Alors, si on choisit de résoudre sur B entre ces deux dernières clauses, nous obtenons ¾®. Nous aurions pu résoudre sur B d'abord, puis sur A, et nous aurions obtenu le même résultat : c'est parce que, pour obtenir la clause vide, nous devons éliminer tous les atomes des clauses par résolution, et nous pouvons le faire dans n'importe quel ordre.

En bref, il n'y a pas vraiment de non-déterminisme dans l'ordre dans lequel nous éliminons les atomes par la règle de résolution, comme tous les ordres doivent donner le même résultat --- la dérivabilité ou l'indérivabilité de la clause vide. (Il s'agit d'un argument de confluence.) Pour éliminer cette redondance, une solution est de fixer un ordre sur les atomes à l'avance, et de ne permettre à la résolution de ne porter que sur les atomes maximaux dans l'ordre.

Figure 3: Séparation simulée par la résolution

La raison pour laquelle cela fonctionne est le fait qu'au niveau propositionnel, la séparation sur A (l'atome maximal) consiste à calculer tous les résolvants de clauses sur A. Regarder la figure 3 : écrivons S comme l'union de trois ensembles : l'ensemble S_A des clauses de la forme A Ú C, autrement dit les séquents avec A à droite; l'ensemble S_{¬
A} des clauses de la forme ¬ A Ú C, autrement dit les séquents avec A à gauche; et l'ensemble S_Ø de toutes les clauses où A et ¬ A n'apparaissent pas. Nous supposons que les tautologies ont été éliminées, et donc ces trois ensembles sont disjoints. Soit S'_A l'ensemble S_A d'où A a été effacé, et de même pour S'_{¬ A} et S_{¬ A}.

Observer que S[T/A] est précisément l'ensemble des clauses de S'_{¬ A} et S_Ø. Intuitivement, S[T/A] = S'_{¬ A} Ù S_Ø; et de même, S[F/A] = S'_A Ù S_Ø. La méthode de Davis-Putnam cherche une interprétation satisfaisant S[T/A] ou S[F/A]. C'est une façon de chercher une interprétation satisfaisant S[T/A]Ú S[F/A]. Ce dernier est, intuitivement, S_ØÙ (S_A Ú S_{¬ A}). Et S_A Ú S_{¬ A} est juste, par distributivité, la même chose que l'ensemble des résolvants entre clauses de S sur A et ¬ A.

Au niveau propositionnel, nous pouvons éliminer les atomes dans n'importe quel ordre. Autrement dit, nous pouvons nous donner un ordre sur les atomes, et toujours éliminer le plus grand. Tous les ordres ne fonctionnent pas au premier ordre, cependant, c'est pourquoi nous définissons :

Définition 20  [Stabilité]   Un ordre strict > sur les atomes est dit stable si et seulement si pour tous atomes A, B, et pour toute substitution s, A > B implique As > Bs.

Rappelons qu'un ordre strict est une relation irréflexive et transitive. Les ordres stricts stables sont aussi appelés A-ordres (``A-orderings'') dans la littérature.

Un ordre strict stable ne peut pas être total en général. En effet, si P(x) > P(y), par exemple, alors on doit aussi avoir P(y) > P(x), par la substitution [x/y,y/x]. Comme nous voulons restreindre les atomes sur lesquels nous résolvons aux atomes maximaux pour >, il est intéressant d'avoir le moins de choix possible, c'est-à-dire d'avoir aussi peu d'atomes incomparables que possible. Résoudre ce problème est encore impossible en général, mais nous pouvons améliorer> en le forçant à avoir la propriété suivante :

Définition 21  [Totalité sur les termes clos]   Un ordre strict > est dit total sur les termes clos si et seulement si pour tous atomes clos A et B, on a A<B, ou A=B, ou A>B.

Les ordres totaux sur les termes clos existent, par exemple les ordres récursifs sur les chemins (``recursive path ordering'' ou rpo) [DJ90] fondés sur une précédence totale. Nous définissons alors le raffinement suivant de la résolution :

Définition 22  [Stratégie ordonnée]   Soit > un ordre strict stable sur les atomes (possiblement, et préférablement, total sur les termes clos). Soit >^# la relation définie par s >^#t si et seulement si s>t ou s et t sont incomparables pour >, ou de façon équivalente si non s < t. Nous disons qu'un atome A est maximal dans un ensemble S d'atomes si et seulement si A >^#B pour tout BÎ S\{A}, c'est-à-dire si et seulement si A est plus grand que tout atome qui lui est comparable dans S, c'est-à-dire qu'aucun autre atome n'est plus grand que A dans S.

La stratégie ordonnée est le raffinement de la résolution où les facteurs de clauses C sont calculés en n'unifiant que les atomes maximaux de C, et où les résolvants binaires de clauses C et C' sont calculés en unifiant des littéraux complémentaires maximaux dans leurs clauses respectives.

Théorème 23  [Complétude]   La stratégie ordonnée est correcte et complète.
Preuve : Elle est clairement correcte, en tant que restriction de la résolution, qui est correcte. Elle est complète au niveau des atomes clos (au niveau propositionnel). En effet, nous invoquons l'argument ci-dessus pour simuler Davis-Putnam par la résolution. Mais il y a encore un léger problème : lorsque A ou ¬ A est pur, c'est-à-dire quand S_{¬ A} ou S_A est vide, il n'y a aucun résolvant sur A. Par exemple, A est pur dans l'ensemble des trois clauses A ¾® B, ¾® B et B¾®, donc il n'y a pas de résolvant sur A; mais cet ensemble de clauses est quand même insatisfiable : il suffit de résoudre sur B à la place. Nous devons donc ignorer les clauses pures dans la preuve. Soit S un ensemble insatisfiable fini de clauses closes. Nous simulons la règle de séparation de Davis et Putnam sur l'atome non pur A en calculant l'ensemble de tous les résolvants de clauses dans S sur A; soit S(A) ce dernier ensemble. Alors S(A) est une forme normale conjonctive de la disjonction de S[T/A] et S[F/A], en conjonction avec S_Ø, comme illustré sur la figure 3. Comme S est insatisfiable, soit S doit contenir la clause vide, et nous avons fini; soit il existe au moins un atome non pur A dans S, sinon S serait satisfiable. Choisissons A maximal parmi tous les atomes non purs dans S, et calculons S(A) : c'est un ensemble de résolvants ordonnés de S sur A, union le sous-ensemble S_Ø de S. De plus, S(A) contient strictement moins de littéraux purs que S, puisqu'aucun nouveau littéral n'a été créé, et les littéraux purs dans S restent purs dans S(A); et S(A) est clairement insatisfiable.

Cet argument mène à un argument facile de complétude par récurrence sur le nombre d'atomes non purs dans S.

Pour relever le résultat au premier ordre, nous appliquons le théorème de Herbrand : un ensemble S de clauses du premier ordre est insatisfiable si et seulement s'il existe un ensemble fini propositionnellement insatisfiable S' d'instances de clauses de S. Alors, nous pouvons utiliser la résolution ordonnée dans le cas clos pour dériver la clause vide de S', comme nous venons de le montrer. Finalement, cette résolution ordonnée close peut être simulée par des étapes de résolution au premier ordre comme au théorème 9, et ces étapes de résolution sont des étapes de résolution ordonnée, parce que > est stable. ¤

La résolution ordonnée est compatible avec l'élimination de tautologies, de clauses subsumées et de clauses pures. En d'autres termes, la combinaison de ces techniques fournit encore une procédure complète de réfutation. En fait, la preuve ci-dessus montre que l'élimination des clauses pures est compatible avec la stratégie ordonnée. En ce qui concerne la subsomption et l'élimination de tautologies, la clef est que le lemme 12 continue de s'appliquer dans le cas ordonné, parce que par stabilité de l'ordre, tout littéral maximal dans une clause G', G s ¾® D s, D' subsumée par G ¾® D est dans G', D' ou est une instance d'un littéral maximal de G ¾® D.

4.4 Résolution sémantique et stratégies d'ensemble de support

Figure 4: I-conflit en résolution sémantique

Les résolutions sémantiques guident les règles de résolution au moyen d'une interprétation I. Considérons la procédure de Davis-Putnam de nouveau. Dans le cas clos (propositionnel), la stratégie ordonnée revient à fixer un ordre sur les atomes clos A₁, A₂, ..., A_n; nous séparons alors sur A₁, puis sur A₂, et ainsi de suite. Les résolutions sémantiques contrôlent quelle branche nous explorons d'abord à chaque séparation. Chaque fois que nous souhaitons séparer sur A_i, nous pouvons essayer d'explorer le cas A_i vrai d'abord, puis le cas A_i faux; ou bien le contraire. Nous pouvons coder ce choix par une interprétation I : si I rend A_i vrai, alors nous choisissons d'explorer le cas A_i vrai d'abord, sinon nous explorons le cas A_i faux d'abord.

Disons que I satisfait une clause C si et seulement si elle satisfait C pour toutes les affectations possibles de ses variables libres. Autrement dit, si x₁, ..., x_n sont les variables libres de C, si elle satisfait la clôture universelle " x₁ · ... · " x_n · C de C. Un autre point de vue sur la résolution sémantique est le suivant.

Supposons par exemple que notre ensemble initial de clauses S consiste en, tout d'abord, un ensemble S' de clauses exprimant un certain nombre d'axiomes de l'arithmétique, et ensuite, un ensemble S'' de clauses représentant la version skolémisée de la négation d'une proposition à prouver dans le système S'. Comme l'arithmétique est cohérente, elle a un modèle I, à savoir l'ensemble N des entiers naturels muni des opérations usuelles. Nous pouvons alors utiliser ce modèle I pour nous guider au travers de la preuve de notre proposition. L'idée de la résolution sémantique est d'essayer de reconnaître quelles clauses sont déjà satisfaites par I, et d'interdire toutes les étapes de résolution entre deux de ces clauses. Intuitivement, cela ne nous aiderait pas à progresser vers la dérivation de la clause vide, car nous ne pouvons pas la dériver à partir d'un ensemble satisfiable de clauses.

N'importe quelle interprétation auxiliaire convient pour la résolution sémantique. Une des interprétations les plus simples est l'interprétation de Herbrand positive dans laquelle tous les atomes clos sont supposés vrais. Alors I satisfait une clause C si et seulement si son côté droit est non vide. Nous appelons une telle clause G¾®, qui n'est pas satisfaite par l'interprétation positive, une clause négative.

De façon symétrique, dans l'interprétation de Herbrand négative, tous les atomes clos sont supposés faux. Dans cette interprétation, une clause est satisfaite si et seulement son côté gauche est non vide, autrement dit si elle n'est pas une clause positive ¾®D.

Tout ceci se résume dans le raffinement suivant de la résolution :

Définition 24 [Résolution sémantique] Soit I une interprétation. Soit A_I un algorithme (terminant) tel que, si A_I retourne ``oui'' sur l'entrée C, alors I satisfait C.

Un I-conflit est un ensemble fini de clauses {N,E₁,..., E_q}, q£ 1, telles que :

A_I retourne ``non'' sur chacune de E₁, ..., E_q;
il existe un résolvant R₁ de N et E₁, un résolvant R₂ de R₁ et E₂, ..., un résolvant R_q de R_q-1 et E_q;
A_I retourne ``oui'' sur R₁, ..., R_q-1, et ``non'' sur R_q.

Les E_i sont appelées les électrons, N est appelée le noyau du I-conflit, et R_q est appelé un I-résolvant du I-conflit.

L'algorithme A_I est la partie bizarre de la définition. Dans l'interprétation positive (resp. négative), il suffit que A_I retourne ``oui'' sur les clauses négatives (resp. positives), et ``non'' sur les autres, et ceci caractérise exactement les clauses qui sont satisfaites par l'interprétation. Mais dans des utilisations plus élaborées de la I-résolution, la satisfaction par I peut ne pas être décidable : dans ce cas, la contrainte que nous imposons à A_I en est une de sécurité. Dans le cas trivial où A_I retourne toujours ``non'' --- un cas vraiment très sûr --- la résolution sémantique n'est rien d'autre que la résolution usuelle, non contrainte, et nous n'avons pas gagné grand chose. Nous souhaiterons donc que A_I retourne ``oui'' sur le plus de clauses possibles.

Voir la figure 4 pour une illustration de ce qu'est un I-conflit. Remarquer que le noyau peut avoir été détecté ou non comme étant satisfait par I. D'une façon plus informelle, la résolution sémantique fonctionne comme suit. Prenons un ensemble S de clauses, et découpons-le en l'ensemble S' des clauses sur lesquelles A_I retourne ``oui'' (l'ensemble des clauses dont on est sûr qu'elles sont satisfaites par I), et en l'ensemble S'' des clauses sur lesquelles A_I retourne ``non'' (l'ensemble des clauses qui ne sont peut-être pas satisfaites par I). Ensuite, choisissons une clause N dans S'È S'', et une clause E₁ dans S'', et résolvons pour produire une nouvelle clause R₁. (Si nous avions choisi N et E₁ venant toutes les deux de S', nous saurions que I satisfaisait R₁, donc ce serait un lemme inutile.) Si A_I retourne ``non'' sur R₁, alors R₁ est possiblement non satisfaite par I, et ceci nous apporte une information nouvelle, donc nous ajoutons R₁ à S'', et ceci termine l'étape de I-résolution. Sinon, nous résolvons entre R₁ et une clause E₂ de S'', ce qui produit R₂, et ainsi de suite jusqu'à ce que nous produisions une clause R_q sur laquelle A_I retourne ``non'', et alors nous ajoutons R_q à S'', ce qui termine l'étape de I-résolution.

En général, cependant, nous ne pouvons pas procéder comme cela, car nous ne connaissons aucune borne a priori sur q, et nous pourrions nous retrouver embarqués dans une boucle infinie, à chercher un I-résolvant sur un mauvais noyau. Nous devrons donc effectuer les recherches sur tous les noyaux possibles en parallèle. En pratique, on n'utilise que de très simples cas de résolution sémantique, comme l'hyper-résolution ou la stratégie d'ensemble de support, où ce problème ne se pose pas. En fait, la résolution sémantique est essentiellement un outil théorique pour explorer des raffinements plus pratiques de la résolution.

Nous montrons le théorème de complétude attendu avant de décrire les examples important sus-mentionnés de résolution sémantique.

Théorème 25  [Complétude]   Étant donnée une interprétation arbitraire I, la I-résolution est correcte et complète.
Preuve : La I-résolution est correcte en tant que restriction de la résolution. Nous affirmons qu'elle est complète, ce que nous montrons dans le cas clos d'abord. Nous relevons ensuite le résultat au premier ordre par le théorème de Herbrand.

Soit S un ensemble fini insatisfiable de clauses closes. Nous montrons par récurrence sur le nombre d'atomes apparaissant dans S que l'on peut dériver la clause vide à partir de S par une réfutation par I-résolution. Si ce nombre est 0, alors S doit être {¾®}, et l'affirmation est prouvée. Sinon, soit A un atome apparaissant dans S, et supposons sans perte de généralité que A est vrai dans I. (Il est sensé de dire que A est vrai ou faux dans I, parce que A est un atome clos.)

Comme S est insatisfiable, S[T/A] est insatisfiable aussi. Par hypothèse de récurrence, il existe une dérivation D₁ de ¾® par I-résolution à partir de S[T/A]. Nous la traduisons en une dérivation D₁' par I-resolution de A ¾® comme suit.

En premier, on peut voir D₁ comme un arbre inversé, où les noeuds sont des clauses, les feuilles sont des clauses dans S[T/A], et la racine est la clause vide ¾®. Construisons D₁' en rajoutant A à gauche des clauses G ¾® D dans S[T/A] aux feuilles qui venaient de clauses A, G ¾® D dans S, et en ajoutant récursivement A à gauche des clauses des noeuds intérieurs si nous l'avions ajouté à gauche d'un de ses parents. (Cette transformation n'est pas nécessairement unique.) D₁' est encore une dérivation par I-résolution, parce que les électrons augmentés par A à gauche restent faux dans I. La conclusion de D'₁ peut être ¾® de nouveau, auquel cas nous avons terminé; ou bien A ¾®, qui est fausse dans I. Supposons ce dernier cas.

Maintenant, comme S est insatisfiable, S[F/A] l'est aussi, donc par hypothèse de récurrence, il existe une réfutation D₂ par I-résolution de S[F/A]. Nous transformons D₂ en une réfutation D'₂ par I-résolution de S È {A ¾®} comme suit. L'idée est de réinsérer A à droite des clauses de D₂, mais ça ne fonctionne pas : certains électrons et certains I-résolvants peuvent devenir vrais dans I. Mais nous pouvons réobtenir une dérivation par I-résolution en résolvant avec l'électron A¾®. Soit N, E₁, ..., E_q un I-conflit arbitraire dans D₂. En ajoutant A à droite de certaines de ces dernières clauses, nous obtenons une suite N', E'₁, ..., E'_q de clauses, où N' est N ou N plus A à droite, et pour tout i, 1£ i£ q, E'_i est soit E_i soit E_i plus A à droite. Pour tout i, si E'_i = E_i, alors E'_i est un électron, et nous ne le modifions pas; sinon, nous remplaçons E'_i par le I-conflit E'_i (noyau), A ¾® (électron) pour déduire E_i (qui est effectivement fausse dans I). Ceci nous permet d'obtenir une suite d'étapes de résolution entre N', E₁, ..., E_q. Si N' = N, alors nous avons reconstruit le I-conflit de D₂. Sinon, nous produisons le I-conflit N', A¾®, E₁, ..., E_q: comme la résolution entre N' et A¾® produit N, cet I-conflit a exactement la même clause finale que N, E₁, ..., E_q. Par récurrence sur la longueur de D₂, nous produisons ainsi une réfutation par I-résolution à partir de S È {A ¾®}. Pour relever le résultat au premier ordre, nous appliquons le théorème de Herbrand : un ensemble S de clauses du premier ordre est insatisfiable si et seulement s'il existe un ensemble fini propositionnellement insatisfiable S' d'instances de clauses de S. Alors nous pouvons utiliser la I-résolution dans le cas clos pour dériver la clause vide de S', comme nous venons de le montrer. Finalement, cette résolution close peut être simulée par des étapes de résolution comme dans le théorème 23, et ces étapes de résolution sont en fait des étapes de I-résolution. En effet, lorsqu'une instance close E' d'une clause E est fausse dans I, alors A_I doit retourner ``non'' sur E : par notre hypothèse de sécurité, si A_I retournait ``oui'', alors E serait satisfaite par I. ¤

Non seulement la résolution sémantique est complète, pour n'importe quelle interprétation I, mais les stratégies d'effacement (tautologies, subsomption, clauses pures) préservent la complétude. Refaisons en effet la preuve du lemme 12 : le point-clé est que si un électron est subsumé par une autre clause, alors cette dernière est aussi un électron, autrement dit elle est falsifiée par I.

Cependant, la résolution sémantique ordonnée n'est pas complète en général (par exemple, l'hyper-résolution positive ordonnée ne peut pas dériver ¾® à partir de l'ensemble insatisfiable de clauses ¾® A, B; B ¾® C; A ¾®; C ¾® dans l'ordre A < B < C; laissé en exercice). Nous pouvons cependant utiliser le raffinement suivant :

Définition 26   La résolution sémantique semi-ordonnée est le raffinement de la résolution sémantique où nous exigeons que le littéral sur lequel on résout à chaque étape soit maximal dans son électron.

Autrement dit, nous exigeons qu'il soit maximal dans chaque E_i, mais pas dans R_i, 1£ i £ q. Alors :

Théorème 27   Étant donnée une interprétation arbitraire I, et n'importe quel ordre strict stable >, la I-résolution semi-ordonnée est correcte et complète.
Preuve : Analogue au théorème 25, à part que nous choisissons A minimal. Lorsque nous ajoutons A à un électron E, le littéral sur lequel on résout dans E reste maximal dans E augmenté par A. De plus, dans A¾®, A est nécessairement maximal. Donc toutes les dérivations qui sont produites dans la preuve sont encore semi-ordonnées. ¤

Il est clair que la résolution semi-ordonnée reste complète lorsqu'on utilise les stratégies d'effacement.

4.4.1 Hyper-résolution

Le premier cas de résolution sémantique est l'hyper-résolution:

Définition 28 [Hyper-résolution] L'hyper-résolution positive est la I-résolution, où les électrons et les résolvants sont contraints à être des clauses positives. (Autrement dit, l'interprétation I est l'interprétation de Herbrand négative.)

L'hyper-résolution négative est la I-résolution, où les électrons et les résolvants sont contraints à être des clauses négatives. (Autrement dit, l'interprétation I est l'interprétation de Herbrand positive.)

Par le théorème 27, les hyper-résolutions positive et negative, et même leurs variantes semi-ordonnées, sont complètes. Pour coder, disons, l'hyper-résolution positive, nous assouplissons la formalisation par noyau et électrons : prenons une clause positive, résolvons-la avec une autre clause, et ajoutons le résolvant à l'ensemble courant de clauses. L'hyper-résolution positive semi-ordonnée consiste alors à ne résoudre que sur les littéraux maximaux dans la clause positive choisie.

Comme Chang et Lee le font remarquer, l'hyper-résolution positive est similaire à la pensée en avant, c'est-à-dire à utiliser des faits disjonctifs (les clauses positives) comme électrons, pour déduire davantage de faits, jusqu'à ce qu'on obtienne la clause vide, c'est-à-dire un ensemble de faits contradictoires. Si nous voulons prouver AÞ B, nous fabriquons une clause ¾® A qui dénote un fait, et une clause B¾® qui représente un but : l'hyper-résolution positive déduira alors des faits à partir de ¾® A, et les annulera en utilisant l'information information négative sur B pour produire la clause vide.

Réciproquement, l'hyper-résolution négative est similaire à la pensée en arrière, c'est-à-dire à réduire le but à prouver en sous-buts, jusqu'à ce qu'il ne reste plus de sous-but. Dans l'exemple ci-dessus, l'hyper-résolution négative fabriquera des clauses négatives à partir de B¾®, jusqu'à ce que tous les sous-buts (les atomes à gauche des clauses négatives) soient prouvés par des faits dérivés de A.

4.4.2 Ensemble de support

L'autre cas important de résolution sémantique est la stratégie d'ensemble de support. L'idée est la suivante : nous ne voulons pas en général prouver des formules isolées F, mais plutôt F, étant donné un ensemble d'axiomes A. Autrement dit, et en supposant que A est fini, nous voulons prouver AÞF, où nous avons noté A la conjonction de tous les axiomes dans l'ensemble A. Nous pouvons usuellement prouver ou au moins supposer que A est cohérent : les axiomes ne sont pas des hypothèses temporaires, ils sont censés décrire un modèle. Le problème alors, si l'on cherche à prouver AÞF, est que la recherche de preuve passera une portion considérable de son temps à réfuter A, et on sait à l'avance --- ou on croit --- que c'est tout à fait inutile. Ceci est particulièrement clair dans le cas de la résolution, où pour prouver AÞF, nous produirions des clauses pour A, et quelques clauses pour ¬F, mais toutes les résolution entre clauses de A sont inutiles !

On peut y remédier en utilisant la résolution sémantique, où l'interprétation guide I est un modèle arbitraire des axiomes. Comme nous ne savons rien à propos de I à l'avance, nous choisissons comme algorithme A_I un des plus simples qui soient sûrs : répondre ``oui'' sur l'entrée C si et seulement si C est une des clauses axiomes.

Puisque A_I est si simple, la stratégie d'ensemble de support peut être réalisée comme suit : diviser l'ensemble initial S en deux sous-ensembles disjoints S' (l'ensemble des clauses venant des axiomes dans A) et S'' (les autres clauses, correspondant à la négation du but F à prouver). L'ensemble S'' est alors l'ensemble de support pour le processus de résolution. Maintenant, nous appliquons la résolution répétitivement, en sélectionnant des clauses parentes de sorte qu'au moins une des clauses parentes vienne de l'ensemble de support S'', et nous ajoutons les résolvants à l'ensemble de support S''. (Remarquer que l'on peut aussi coder l'hyper-résolution comme ceci, et en fait n'importe quelle résolution sémantique.)

En tant que cas particulier de résolution sémantique, la stratégie d'ensemble de support est complète, pourvu que les axiomes aient au moins un modèle. Nous pouvons aussi utiliser la restriction semi-ordonnée sans perdre la complétude, ainsi que toutes les stratégies d'effacement. En pratique, bien que la résolution sémantique semble prometteuse, elle est considérablement moins efficace que ce à quoi on s'attendrait. Une source possible d'inefficacité est que les résolvants sont toujours mis dans l'ensemble de support S'', et ne sont jamais reconnus comme satisfaits par I, même s'ils le sont : l'algorithme A_I ci-dessus est trop simpliste, et nous aurions réellement besoin d'un algorithme plus spécialisé.

4.5 La stratégie linéaire

La quantité de non-déterminisme dans le choix des clauses à résoudre, même dans les cas de la résolution ordonné ou de la I-résolution semi-ordonnée, peut être terrifiant. Un raffinement de la résolution où ce niveau de non-déterminisme est réduit est la résolution linéaire, où nous choisissons une clause C₀ de l'ensemble de clauses initiales S, nous la résolvons avec une clause pour produire un résolvant C₁, que nous ajoutons à S; nous résolvons ensuite C₁ avec une autre clause pour produire C₂, que nous ajoutons à S, et ainsi de suite, jusqu'à ce que nous obtenions la clause vide.

Figure 5: Résolution linéaire

Le non-déterminisme est réduit, parce qu'un des clauses à résoudre est toujours fixée : c'est la dernière clause que nous avons produite par résolution. Le terme ``résolution linéaire'', qui ne se réfère pas à la logique linéaire, provient de la forme spéciale des dérivations par résolution dans ce cas : voir figure 5. Définissons :

Définition 29 [Résolution linéaire] Une dérivation par résolution linéaire est une dérivation à partir d'un ensemble S de clauses C₀, C₁, ..., C_i, telles que C₀Î S, et pour tout i³ 0, C_i+1 est un résolvant de C_i avec une clause de SÈ{C₁,..., C_i}.

Si C_i+1 est un résolvant de C_i avec une clause C, nous disons que C_i est la clause centrale (``center clause'' en anglais) de l'étape de résolution, C est la clause latérale (``side clause''), et C_i+1 est la nouvelle clause au sommet (``top clause''). Les clauses C₀, ..., C_i sont appelées les clauses ancêtres (``ancestor clauses''). Les clauses de S sont appelées les clauses d'entrée (``input clauses'').

Une dérivation par résolution linéaire est dite semi-ordonnée par rapport à un ordre strict stable > si et seulement si le littéral sur lequel on résout dans la clause centrale est maximal pour >.

Théorème 30 [Complétude] La résolution linéaire (resp. semi-ordonnée) est correcte et complète.
Preuve : Elle est correcte en tant que raffinment de la résolution.

L'idée principale est de rejouer la preuve du théorème 25, en utilisant le fait suivant : étant donné un ensemble insatisfiable fini S de clauses, il existe un ensemble S' de clauses de S qui est minimalement insatisfiable, c'est-à-dire un dont tout sous-ensemble propre est satisfiable. Cet ensemble minimal peut ne pas être unique, mais cela n'a pas d'importance. Sans perte de généralité, supposons que S lui-même est minimalement insatisfiable. Remarquons qu'un ensemble minimalement insatisfiable S de clauses ne peut pas contenir de clauses pures ou de tautologies. Nous en concluons que pour tout atome A apparaissant dans S, A apparaît à gauche d'une clause et à droite d'une autre clause dans S; et que A ne peut pas apparaître à la fois à gauche et à droite de la même clause.

Nous montrons qu'il existe une réfutation par résolution linéaire à partir de S par récurrence sur le nombre d'atomes apparaissant dans S. Si ce nombre est 0, alors S doit être {¾®}, et nous avons fini. Sinon, le résultat est une conséquence du fait plus précis suivant, que nous montrons par récurrence : si S' est un ensemble satisfiable de clauses, et S' È {C₀} est insatisfiable, alors il existe une réfutation par résolution linéaire de S' È {C₀}.

Si C₀ est la clause vide, nous avons fini. Sinon, soit A un atome quelconque apparaissant dans C₀. Sans perte de généralité, supposons que A apparaisse à gauche, autrement dit C₀ est de la forme A, G₀ ¾® D₀.

Comme S est insatisfiable, S[T/A] est insatisfiable aussi, donc par hypothèse de récurrence il existe une réfutation linéaire D₁ de ¾® à partir de S[T/A]. Comme dans la preuve du théorème 25, nous transformons D₁ en une dérivation D'₁ en rajoutant A à gauche de toutes les clauses appropriées dans D₁. D'₁ est une dérivation linéaire, et elle conclut soit ¾® soit A ¾®. Dans le premier cas, nous avons fini, donc supposons que nous sommes dans le deuxième cas.

Maintenant S' È {A ¾®} est aussi insatisfiable, parce que toute interprétation qui satisfait à la fois S' et A¾® satisfait aussi S' et A, G₀ ¾® D₀, c'est-à-dire S. En particulier, (S' È {A ¾®}) [F/A] est insatisfiable, autrement dit S' [F/A] est insatisfiable. Soit S'' un sous-ensemble minimalement insatisfiable de S' [F/A]. Comme S'' est insatisfiable, S'' n'est pas un sous-ensemble de S', qui est satisfiable. Donc il existe une clause C₁ = G₁ ¾® D₁ dans S'' qui n'est pas dans S'. Cette clause doit provenir d'une clause dans S' qui n'est pas C₁, donc de G₁ ¾® D₁, A.

Par hypothèse de récurrence, il existe une réfutation linéaire D₂ de S' [F/A] de clause au sommet initiale C₁. Transformons D₂ en une réfutation linéaire D'₂ de S' È {A ¾®} de clause au sommet initiale A¾® comme suit. D'abord, D'₂ résout la clause au sommet A¾® avec G₁ ¾® D₁, A (qui est dans S'), ce qui produit C₁ comme nouvelle clause au sommet. Si C₁ est la clause vide, nous avons fini. Sinon, la première étape de D₂ était une résolution entre la clause au sommet C₁ et une autre clause C'₁ dans S' [F/A], et produisait une clause C₂ comme nouvelle clause au sommet. Si C'₁ est dans S', alors D'₂ se contente de résdoure entre les deux mêmes clauses pour obtenir la même clause au sommet C₂. Sinon, il existe une clause G₁ ¾® D₁, A dans S' telle que G₁ ¾® D₁ = C'₁. Alors D'₂ résout d'abord entre C₁ et G₁ ¾® D₁, A pour obtenir C₂ avec un A en plus à droite comme nouvelle clause au sommet, et alors nous résolvons cette dernière clause avec la clause ancêtre A ¾® pour réobtenir C₂. Par une récurrence sur la longueur de D₂ (que nous ne formalisons pas ici), nous obtenons ainsi une réfutation linéaire D'₂ de S' È {A ¾®} de clause au sommet initiale A¾®.

La concaténation de D'₁ et de D'₂ fournit alors une réfutation par résolution linéaire de S de clause au sommet initiale C₀, comme annoncé. Nous relevons ensuite le résultat au premier ordre comme d'habitude.

La résolution linéaire semi-ordonnée est complète par un raisonnement analogue : il suffit de choisir pour A un atome minimal, et pour C₀ une clause le contenant, comme dans le théorème 27. ¤

La résolution linéaire n'est pas complète pour n'importe quel choix de C₀; au contraire, il existe un choix de la clause initiale C₀ qui mènera à la clause vide, si S est insatisfiable. Nous pouvons combiner cette stratégie avec celle d'ensemble de support, et choisir C₀ en-dehors de l'ensemble des clauses axiomes. En particulier, si le but est une conjonction universellement quantifiée de formules atomiques, il n'y a qu'une clause non-axiome, et le choix est alors fixé.

Il est aussi possible que la clause au sommet C_i doive être résolue non seulement avec des clauses d'entrée (celles de S), mais aussi avec des clauses ancêtres C_j, 1£ j< i. La restriction de la résolution linéaire où les clauses latérales sont des clauses d'entrée est appelée l'input-résolution. Mais l'input-résolution n'est pas complète. Par exemple, il n'y a pas de réfutation par input-résolution de ¾® A,B, A¾® B, B¾® A, A,B¾®. En fait, il y a une réfutation par input-résolution d'un ensemble S de clauses si et seulement s'il y a une réfutation par résolution unitaire de S (cf. [CL73], pages 134--135), et nous avons déjà vu qu'il n'y avait pas de réfutation par résolution unitaire de ce dernier ensemble de clauses. L'input-résolution est cependant complète pour les ensembles de Horn (les programmes Prolog, en gros).

Finalement, remarquons qu'aucune stratégie d'effacement n'est compatible avec la stratégie linéaire : effacer la clause courante n'aurait pas de sens.

4.6 Autres raffinements de la résolution

Il existe de nombreux autres raffinements de la résolution. Consulter [CL73] pour un panorama, ainsi que pour les raisons détaillées pour lesquelles ils fonctionnent et comment.

La résolution ordonnée peut être définie au moyen de différentes notions d'ordre. La lock-résolution de Robert Boyer, par exemple, (cf. [CL73]), affecte des rangs arbitraires à chaque occurrence de littéraux dans les clauses.

Une variante intéressante de la résolution linéaire appelée OL-résolution (pour ordonnée linéaire, mais ce n'est pas exactement ce que nous avons appelé résolution ordonnée linéaire en section 4.5), est la résolution linéaire où les clauses sont codées comme des listes de littéraux sans répétition; l'ordre dans lequel les littéraux apparaissent joue le rôle de l'ordre sur les atomes que nous avons utilisé pour restreindre les dérivations par résolution. La méthode est complète. De plus, des techniques de codages intelligentes peuvent être utilisées pour ne représenter que la clause au sommet C_i, qui codent les clauses centrales C₁, ..., C_i-1 à l'intérieur de C_i. (Voir [CL73], section 7.4.) Nous verrons au prochain chapitre comment cette technique peut en fait être vue comme une technique de tableaux.

La résolution à graphe de connexions (``connection graph resolution'') de Robert Kowalski est plus élaborée, car elle est à la fois une réalisation particulière et une méthode pour empêcher la génération de nombreuses clauses inutiles. Dans cette méthode, les paires unifiables de littéraux complémentaires sont représentées par des liens, c'est-à-dire des arêtes dans un graphe de clauses; les résolvants héritent implicitement les liens de leurs clauses parentes, de sorte que le nombre d'unifications à effectuer est minimisé. Une clause possédant un littéral sans lien est pure, et est immédiatement éliminée. Ceci peut ensuite couper d'autres liens, ce qui crée de nouvelles clauses pures, et ainsi de suite. Pour éviter les redondances, une fois qu'un lien a été utilisé pour produire un résolvant, il est coupé pour qu'il ne puisse pas être réutilisé. C'est une réalisation très efficace de la résolution. Cependant, le fait de couper les liens utilisés peut faire perdre la complétude en présence de certaines stratégies; et lorsque la résolution à graphe de connexions est complète, la preuve de complétude est en général complexe.

Ces problèmes sont résolus dans la soustraction d'instances de Jean-Paul Billon, mais la soustraction d'instances ne fonctionne pas avec la résolution. À la place, Billon code la soustraction d'instances au-dessus du calcul de Lee et Plaisted [LP92], où ce sont des instances de clauses, pas des résolvants, qui sont produits au moyen de la règle :

CÙ A	¬ A' Ù C'

(CÙ A)s	(¬ A' Ù C')s

où les clauses sous la ligne sont ajoutées à l'ensemble courant de clauses, et s est le mgu de A et A'. Cette idée de Lee et Plaisted permet au prouveur de découpler la tâche de recherche d'unificateurs (par unification de littéraux complémentaires) de la tâche consistant à montrer que l'ensemble de clauses close sous-jacent est propositionnellement insatisfiable. Cette second tâche peut être laissée à n'importe quelle méthode propositionnelle, incluant la résolution, mais pas uniquement la résolution.

Au-dessus de ce calcul, l'idée de Billon est d'attacher à chaque clause un ensemble de substitutions qui ont été utilisée pour produire des instances, et qui ne doivent pas être réutilisées. Ceci évite d'engendrer la même clause plusieurs fois dans la plupart des cas. Au lieu de couper des liens, elle interdit les unifications le long des liens précédents en comparant les substitutions. C'est plus général que la technique de Kowalski, puisque cela ne se limite pas à couper le lien sur lequel on a résolu, et il est plus facile de montrer que c'est complet. Billon a depuis considérablement amélioré l'idée au point que l'on n'a même plus besoin d'enregistrer ces substitutions, en utilisant intelligemment une notion de chemins à travers l'ensemble des clauses [Bil96].