5 Hyperrésolution semi-ordonnée
Nous pouvons tenter de combiner les restrictions de
l'hyperrésolution et de la résolution ordonnée, mais le faire
naïvement mène à l'échec. L'exemple :
A Ú B A Ú ¬ B ¬ A Ú B ¬ A Ú ¬ B
avec A < B ne permet de résoudre qu'avec le fait A Ú B par
hyperrésolution, et uniquement sur le littéral B par la
contrainte d'ordre. On ne peut donc déduire que A (avec la
règle A Ú ¬ B) ou A Ú ¬ A (avec la règle ¬ A
Ú ¬ B). Le fait A ne peut maintenant être utilisé
qu'avec la règle A Ú ¬ A si nous voulons respecter les
contraintes d'ordre, et ceci ne fait que régénérer le fait A.
L'hyperrésolution positive ordonnée n'est donc pas complète.
Mais on peut quand même poser une contrainte d'ordre, du moment
qu'elle ne porte que sur une des deux prémisses. La règle d'hyperrésolution positive semi-ordonnée à laquelle nous
aboutissons est la suivante :
Pour montrer la complétude, nous procédons comme pour
l'hyperrésolution positive. Mais au lieu de partir d'une
réfutation quelconque, nous partons d'une réfutation ordonnée.
Les règles (1)-(3) peuvent produire des réfutations qui ne sont
plus ordonnées, par exemple (1) lorsque A < B détruit la
contrainte d'ordre; c'est normal, sinon nous pourrions prouver que
l'hyperrésolution ordonnée est complète. Mais la propriété
d'être positivement semi-ordonné est, elle, préservée :
Lemme 10
On dit qu'une dérivation p par résolution est positivement semi-ordonnée si et seulement si toute coupure
de p :
est telle que A est maximal dans C. (Noter que les
dérivations par hyperrésolution positive semi-ordonnée sont
exactement les dérivations par hyperrésolution positive qui sont
positivement semi-ordonnées.)
Si p se réécrit en p' par l'une des règles (1)-(3),
alors p' est positivement semi-ordonnée.
Preuve : Par récurrence structurelle sur p, les seuls cas
intéressants étant ceux où p est l'un des rédex
possibles.
Règle (1) : comme p est positivement semi-ordonnée, A
est maximal dans C, B est maximal dans C'1 Ú ¬ A. En
particulier : (a) B est maximal dans C'1, et : (b) B > A.
Comme A est maximal dans C, (b) implique que B est maximal
dans C; et par (a), nous déduisons : (c) B est maximal dans C
Ú C'1. Comme A est maximal dans C, et que p0,
p1, p2 sont positivement semi-ordonnées parce que p
l'est, le côté droit de la règle est donc bien positivement
semi-ordonné.
Règle (3) : raisonnement similaire.
Règle (2) : comme p est positivement semi-ordonnée, A
est maximal dans C, B est maximal dans C1, et p0,
p1, p2 sont positivement semi-ordonnées : le côté
droit de la règle est donc bien positivement semi-ordonné.
¤
Théorème 11
L'hyperrésolution positive semi-ordonnée est complète.
Preuve : Soit S un ensemble de clauses insatisfiable. Par le
théorème 9, il existe une réfutation p par
résolution ordonnée de S, et donc en particulier par
résolution semi-ordonnée. Par le lemme 6,
p a une forme normale p' pour la relation de réécriture
définie par les règles (1)-(3), qui est une réfutation de
S. Par le lemme 5, p' est une réfutation
par hyperrésolution positive. Par le lemme 10,
p' est positivement semi-ordonnée.
¤