Remarques

6 Remarques

6.1 L'hyperrésolution fait plus

Soit C une clause positive (un fait) dérivable à partir de S par résolution. Alors C est aussi dérivable de S par hyperrésolution positive. En une phrase :

L'hyperrésolution positive dérive tous les faits dérivables.

Ceci généralise le corollaire 7, qui était le cas particulier où C était la clause vide. La seule chose à changer dans la démonstration de la section 3 est le lemme 5, qui doit être étendu à toute dérivation p d'une clause positive à partir de S; dans la preuve, la phrase ``En particulier, C₁ Ú C₂ n'est pas la conclusion de p, qui est la clause vide'', conséquence du fait que C₁ Ú C₂ n'est pas positive, doit être remplacée par ``En particulier, C₁ Ú C₂ n'est pas la conclusion de p, qui est par hypothèse une clause positive''.

6.2 Hyperrésolution négative

Il n'y a rien de magique à choisir des clauses positives dans l'hyperrésolution. En fait, on peut aussi considérer l'hyperrésolution négative :

sachant qu'une clause négative est une clause de la forme ¬ A₁ Ú ... Ú ¬ A_n. Une telle clause est la négation d'un but ¬ (A₁ Ù ... Ù A_n), et si l'on peut voir l'hyperrésolution positive comme dérivant de nouveaux faits à partir des anciens (démonstration en avant), l'hyperrésolution négative peut être vue comme réduisant d'anciens buts à de nouveaux sous-buts (en arrière).

L'hyperrésolution négative, et l'hyperrésolution négative semi-ordonnée sont complètes aussi. Considérons en effet la transformation S |® S^- qui remplace dans S tout littéral négatif ¬ A par A et tout littéral positif A par ¬ A. Si S est insatisfiable, alors S^- est aussi insatisfiable : en effet, si on avait r |= S^-, alors on aurait r' |= S, où r' envoie tout A vers la négation de r (A). Donc S^- a une réfutation par hyperrésolution positive (resp. semi-ordonnée). Appliquons la transformation inverse S |® S^- à toute cette réfutation : il est facile de voir que l'on obtient ainsi une réfutation de S d'une part, et qu'il s'agit d'une réfutation par hyperrésolution négative (resp. semi-ordonnée), la transformation transformation en effet les clauses positives en négatives et vice-versa.

6.3 Résolution sémantique

On peut généraliser la remarque 6.2 comme suit. Notons que les clauses positives sont exactement les clauses qui sont rendues fausses par l'affectation l A · F, et les clauses négatives sont exactement les clauses qui sont rendues fausses par l'affectation l A · T. En général, donnons-nous une affectation r₀, et considérons la règle :

où l'une des prémisses est contrainte à être fausse dans r₀. Cette règle s'appelle la résolution sémantique, ou r₀-résolution.

La résolution sémantique est complète, par un argument similaire à celui utilisé ci-dessus pour l'hyperrésolution négative. Considérons la transformation S |® S^r₀ qui, pour tout A tel que r₀ (A) = T, transforme A en ¬ A et ¬ A en A, mais ne change pas les A tels que r₀ (A) = F. Si S est insatifiable, alors S^r₀ aussi; en effet, si on avait r |= S^r₀, alors l'interprétation r' envoyant A vers r (A) si r₀ (A) = F et A vers non r (A) si r₀ (A) = T serait telle que r' |= S. Donc S^r₀ a une réfutation par hyperrésolution positive. Appliquons la transformation inverse S |® S^r₀ à toute cette réfutation : il est facile de voir que l'on obtient ainsi une réfutation de S d'une part, et qu'il s'agit d'une réfutation par r₀-résolution d'autre part. En effet, toute clause positive A₁ Ú ... Ú A_m Ú B₁ Ú ... Ú B_n (où sans perte de généralité on a choisi les A_i tels que r₀ (A_i) = T et les B_j tels que r₀ (B_j) = F) se traduit en ¬ A₁ Ú ... Ú ¬ A_m Ú B₁ Ú ... Ú B_n, qui est rendue fausse par r₀.

De façon similaire, la résolution sémantique semi-ordonnée, où l'une des prémisses est contrainte à être fausse dans r₀ et la formule de coupure doit être maximale dans l'autre prémisse, est encore complète.

6.4 Résolution ordonnée avec un ordre partiel

Nous avons montré que les restrictions d'ordre étaient complètes lorsque < était un ordre total. En fait, elles fonctionnent toujours même lorsque < est un ordre partiel. En effet, tout ordre partiel < peut être plongé dans un ordre total <⁺, autrement dit : il existe un ordre total <⁺ tel que pour tous A, B, A < B implique A <⁺ B. (Ce résultat nécessite l'axiome du choix dans le cas général; ici, nous n'en avons besoin que sur des ensembles finis d'atomes, et une simple récurrence suffit.) Un littéral A ou ¬ A maximal dans une clause C est alors défini par : pour aucun B ou ¬ B dans C, on n'a A < B. Les notions de résolution ordonnée, hyperrésolution semi-ordonnée, etc., s'en trouvent conséquemment modifiées. Tout littéral maximal pour < est alors aussi maximal pour <⁺, et nous concluons à la complétude en observons que toute résolution ordonnée, hyperrésolution semi-ordonnée, etc., pour l'ordre <⁺ en est encore une pour l'ordre <.

6.5 Tautologies, clauses pures et subsumées, suite

On peut montrer que l'élimination de clauses tautologiques, pures et subsumées est compatible avec tous les raffinements de la résolution présentés ici. Autrement dit, combiner les techniques préserve la complétude. Les preuves sont comme en section 2, en adaptant la notion de dérivation par résolution au cas des dérivations par hyperrésolution, par résolution ordonnée, etc.

Il existe des raffinements de la résolution pour lesquels l'élimination de tautologies, de clauses pures ou subsumées casse la complétude, comme la lock-résolution de Boyer.

6.6 Et la sémantique, dans tout ça ?

Bizarrement, nous avons prouvé que l'hyperrésolution, l'hyperrésolution semi-ordonnée et même la résolution sémantique étaient complètes par des moyens complètement syntaxiques. Par contre, nous avons été capables de montrer la complétude de la résolution ordonnée par un moyen sémantique (par arbres de décision). Il ne semble pas y avoir de démonstration sémantique de la complétude des méthodes précédentes.

6.7 Ensemble de support

Un cas particulier de la résolution sémantique est celui de la restriction dite de l'ensemble de support (set-of-support strategy). Supposons que l'ensemble de clauses S à réfuter soit de la forme S₀ È S₁, où S₀ est un ensemble non contradictoire de clauses. Le point est que l'on ne souhaite pas exhiber d'affectation satisfaisant S₀, mais il en existe une, nommons-la r₀. Ce cas peut se présenter par exemple lorsque S₀ est un ensemble d'instances d'une théorie modélisant un phénomène réel (l'univers fournissant le modèle r₀, mais r₀ est en général trop compliqué à décrire).

Si S est contradictoire, alors par la remarque 6.3, il existe une r₀-réfutation de S. Dans une telle réfutation sémantique, il est impossible que les deux prémisses d'une coupure soient prises dans S₀, puisque r₀ satisfait toutes les clauses de S₀. On peut donc restreindre la règle de résolution à ne résoudre qu'entre deux clauses, dont au plus une vient de S₀, et à rajouter le résolvant à l'ensemble S₁. (S₁ est appelé l'ensemble de support.)

Encore une fois, on peut se restreindre à ne résoudre que sur un littéral maximal dans toute clause de S₀. Mais la résolution par ensemble de support peut engendrer beaucoup plus de clauses que la r₀-résolution pour peu que l'on connaisse explicitement r₀, même avec la restriction ordonnée.

6.8 Résolution linéaire

Un autre raffinement important de la résolution est la résolution linéaire. Les transitions de cette forme de résolution sont de la forme :

S, C₀ ® S È {C₁}, C₁

où C₀ est une clause de S, C₁ est un résolvant de C₀ avec une clause C de S. C₀ est appelée la clause centrale, C est la clause latérale, et C₁ est la nouvelle clause au sommet. L'idée est que l'on choisit une clause dans l'ensemble initial S₀ de clauses, qui devient la clause au sommet, et on ne s'autorise à fabriquer la prochaine clause au sommet qu'en résolvant la précédente avec soit une clause de S₀ (une clause input) soit une clause précédemment générée (une clause ancêtre).

La résolution linéaire est complète, même dans sa variante semi-ordonnée (où la formule de coupure doit être maximale dans la clause latérale). Mais elle n'est pas compatible avec la stratégie de subsomption des nouvelles clauses, notamment.