Résolution ordonnée

4 Résolution ordonnée

Un autre raffinement classique de la résolution est la résolution ordonnée. Considérons, comme dans les BDD, que nous nous sommes donné un ordre total < sur les atomes. Supposons que S est un ensemble insatisfiable de clauses, et numérotons les atomes libres dans S A₁ < A₂ < ... < A_n. Si nous reprenons la preuve sémantique de la complétude de la résolution, il est facile de voir que pour tout noeud d'inférence n étiqueté par A_j, de fils les noeuds d'échec n₁ et n₂ pour les clauses C Ú A_j et C' Ú ¬ A_j respectivement, alors l'étape de résolution qui transforme n en un nouveau noeud d'échec :

est telle que A_j est maximal dans C et dans C' : tous les A_i dans C et dans C' doivent être tels que i < j. La preuve de complétude de la résolution s'adapte ainsi directement pour montrer la complétude de la règle de résolution ordonnée :

Par exemple, pour montrer que :

A Ú B A Ú ¬ B ¬ A Ú B ¬ A Ú ¬ B

est insatisfiable, si on se fixe l'ordre A<B, ceci nous interdit de résoudre A Ú B et ¬ A Ú B. Par contre, on peut résoudre AÚ B et A Ú ¬ B sur B, donnant A; puis ¬ A Ú B et ¬ A Ú ¬ B sur B, donnant ¬ A. Et maintenant A et ¬ A sur A, donnant la clause vide.

Il est aussi possible de montrer la complétude de la résolution ordonnée par transformation de preuves. C'est en fait beaucoup plus simple que pour l'hyperrésolution.

Comme pour le lemme 5, nous remarquons :

Lemme 8 Soit p une réfutation par résolution à partir de S. Si p n'est pas obtenue par résolution ordonnée, alors p contient un rédex de la forme :

où B n'est pas maximal dans C₁ ou C₂, et A est maximal dans C et C'.
Preuve : Comme pour le lemme 5. Comme p n'est pas obtenue par résolution ordonnée, elle contient une coupure entre deux clauses sur un B non maximal. Choisissons une occurrence minimale d'une telle coupure, c'est-à-dire la plus basse possible dans p :

avec B non maximal dans C₁ ou C₂. En particulier, il existe un littéral supérieur à B dans C₁ ou dans C₂, donc dans C₁ Ú C₂. Donc C₁ Ú C₂ n'est pas la clause vide, et nous concluons comme au lemme 5. ¤

Notons en particulier que B < A. En effet, B n'est pas maximal dans C₁ ou C₂, donc il existe un littéral supérieur à B dans C₁ Ú C₂. Mais A est maximal dans C₁ Ú C₂, donc A > B.

Comme en hyperrésolution, le littéral A ou ¬ A dans C₁ Ú C₂ peut provenir de C₁, de C₂, ou des deux. Ceci mène aux six règles de réduction (1)-(3) (cf. section 3) plus les suivantes, obtenues par remplacement de A par ¬ A et réciproquement dans (1)-(3), soumises à la condition que B < A :

Pour montrer la terminaison, on utilise la traduction suivante T_ord définie par T_ord (C) = a si C est un axiome dans S (une preuve sans prémisse), et :

où les symboles de fonction f_A sont indicés par les formules de coupure A. Via la traduction T_ord, nous sommes ramenés à montrer que le système de réécriture suivant termine :

(1)	f_A (t₀, f_B (t₁, t₂))	®	f_B (f_A (t₀, t₁), t₂)
(2)	f_A (t₀, f_B (t₁, t₂))	®	f_B (t₁, f_A (t₀, t₂))
(3)	f_A (t₀, f_B (t₁, t₂))	®	f_B (f_A (t₀, t₁), f_A (t₀, t₂))
(4)	f_A (f_B (t₁, t₂), t₀)	®	f_B (f_A (t₁, t₀), t₂)
(5)	f_A (f_B (t₁, t₂), t₀)	®	f_B (t₁, f_A (t₂, t₀))
(6)	f_A (f_B (t₁, t₂), t₀)	®	f_B (f_A (t₁, t₀), f_A (t₂, t₀))

ü
ï
ï
ï
ý
ï
ï
ï
þ

(A > B)

Il suffit de prendre un rpo fondé sur la précédence > définie par f_A > f_B ssi A > B. Cette précédence est bien fondée sur l'ensemble fini des atomes libres dans S. Nous en concluons pour la seconde fois :

Théorème 9 La résolution ordonnée est complète.