2 Tautologies, subsomption, clauses pures
Nous identifions dans la suite les notions de clauses et de
séquents. Considérons les types suivants de clauses :
Une tautologie est une clause contenant à la fois un atome
A et sa négation ¬ A.
On dit qu'une clause C est subsumée par une clause C' si
et seulement si C = C' Ú C'' (en abrégé, C' Í C)
pour une certaine clause C''. En particulier, C est impliquée
par C'.
Une clause C est pure dans l'ensemble de clauses S si et
seulement si C contient un littéral A tel que ¬ A
n'apparaisse dans aucune clause de S, ou bien un littéral ¬ A
tel que A n'apparaisse dans aucune clause de S.
Intuitivement, les tautologies, les clauses subsumées par d'autres
clauses, les clauses pures sont sémantiquement inutiles ou
redondantes. On peut donc déjà les effacer de l'ensemble initial
de clauses S.
Ce qu'on peut se demander, c'est s'il est légal d'effacer de telles
clauses lorsqu'elles se retrouvent générées par l'algorithme de
résolution. En effet, on peut imaginer la situation suivante : sans
effacer les clauses inutiles ou redondantes, supposons qu'il faille 3
étapes de résolution pour réfuter S. Fabriquons un
résolvant et ajoutons-le à S, nous sommes à deux étapes de
la clause vide. Maintenant supprimons par exemple une clause
subsumée de S : il est envisageable que, bien que S reste
insatisfiable, il nous faille maintenant 4 étapes de résolution
pour réfuter S. Si le processus continue, nous engendrerons des
ensembles de clauses qui, même s'ils sont tous insatisfiables,
s'éloigneront petit à petit d'un ensemble contenant la clause
vide, au lieu de s'en rapprocher.
Il est plus commode ici d'abandonner pour un temps la présentation
de la résolution en terme de preuves formées uniquement avec des
clauses de S et des coupures. Rappelons qu'une étape de
résolution à partir de S est une transition :
S ® S È {C Ú C'}
où le résolvant CÚ C' est obtenu à partir de deux clauses
C Ú A et C' Ú ¬ A de S.
Une dérivation par résolution de la clause C0 à partir de S
est une suite finie d'étapes de résolution :
S = S0 ® S1 ® ... ® Sn ' C0
Il s'agit d'une réfutation de S si C0 est la clause
vide.
Il est facile de voir que l'on peut toujours transformer une
dérivation par résolution en ce sens en une dérivation par
coupures au sens de la section 1 (par récurrence sur
n), et réciproquement. L'unique différence est que les
dérivations vues en tant que suites d'étapes peuvent être
beaucoup plus courtes que les dérivations par coupures, parce
qu'elles partagent systématiquement les sous-dérivations. Par
exemple, considérons l'ensemble de clauses :
S0 = {A Ú D, A Ú ¬ D, ¬ A Ú B, ¬ A Ú E, ¬ B Ú ¬ E}
S0 est insatisfiable : résoudre A Ú D avec A Ú ¬ D,
pour obtenir A, ceci produit S1 = S0 È {A}. Puis
résoudre A et ¬ A Ú B, pour obtenir S2 = S1 È
{B}; résoudre A encore avec ¬ A Ú E, pour obtenir S3
= S2 È {E}; résoudre B avec ¬ B Ú ¬ E pour
obtenir S4 = S3 È {¬ E}, enfin résoudre avec E pour
obtenir S5 qui contient la clause vide. Mais une représentation
par preuve avec coupures duplique la dérivation de A à partir de
A Ú D et A Ú ¬ D :
Ceci étant dit, examinons l'effet de la subsomption :
Lemme 1
Soient deux clauses C1 et C'1, et supposons que C1 subsume
C'1. Pour tout résolvant C' entre C'1 et C2, C' est
subsumée par C1 ou par un résolvant de C1 et C2.
De plus, l'unique clause qui subsume la clause vide est la clause
vide.
Preuve : Posons C'1 = C1 Ú C'. Supposons que la formule de coupure
intervienne en tant que ¬ A dans C2 (le cas A est
similaire), et en tant que A dans C'1. Alors C2 est de la
forme C'2 Ú ¬ A. Si A est dans C', alors C' est de
la forme C'' Ú A, donc C' = C1 Ú C'' Ú C'2 est
subsumée par C1. Sinon, alors C1 est de la forme C'' Ú
A, et C' = C'' Ú C' Ú C'2, qui est subsumée par le
résolvant C'' Ú C'2 de C1 = C'' Ú A et de C2 = C'2
Ú ¬ A.
¤
Il s'ensuit :
Corollaire 2
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 n étapes
de résolution, alors elle est dérivable à partir de S' en
au plus n étapes de résolution.
Preuve : Par récurrence sur n. Si n=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 n-1 étapes, et que nous puissions dériver la clause
vide de S en n étapes, n>0. Examinons la première étape
de résolution dans la dérivation : nous résolvons deux clauses
C1 et C2 pour produire le résolvant C.
Par hypothèse, C1 est subsumée par une clause C'1 de S'
(éventuellement C1 elle-même), et C2 est subsumée par
une clause C'2 de S'. Par le lemme 1, C
est subsumée par une clause C', qui peut être C'1, C'2
ou un résolvant de C'1 et C'2. 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 n-1 étapes de SÈ{C}. Par hypothèse de récurrence,
nous pouvons dériver la clause vide en au plus n-1 étapes de
S'È{C'}, donc en au plus n étapes de S'.
¤
Nous pouvons ainsi conclure qu'il est légal de supprimer les clauses
subsumées. Appelons distance de S à la clause vide la
plus petite longueur n d'une réfutation à partir de S.
Supposons S0 à distance n de la clause vide. Supprimer toutes
les clauses subsumées de S0, une à une (pas en parallèle !),
produit un sous-ensemble S'0 de S0 qui est à distance au plus
n de la clause vide, par le corollaire 2. Donc
soit la clause vide est dans S'0, donc dans S0, soit il existe
une étape de résolution menant de S'0 à un ensemble de
clauses S1 à distance au plus n-1 de la clause vide. Par
récurrence sur n, nous montrons ainsi facilement que pour toute
stratégie d'élimination des clauses subsumées, la clause vide
est toujours accessible en au plus n étapes de résolution.
On peut presque voir pourquoi on peut éliminer les clauses
subsumées en format par coupures. En particulier, le cas suivant
est particulièrement clair :
lorsque C, subsumée par C', est obtenue comme conclusion d'une
sous-preuve de celle qui conclut C'. Comme on peut permuter les W
vers le bas sans augmenter la taille de la preuve, et comme il ne peut
subsister d'instances de W en bas de la preuve, cette opération
diminue strictement la taille de la preuve. Mais cette explication ne
fonctionne que si C est au-dessus de C', pas à côté par
exemple.
Quant aux tautologies, nous avons :
Lemme 3
Soit C une tautologie. Alors tout résolvant de C avec
n'importe quelle clause C' est une tautologie ou est subsumée
par C'.
Preuve : Soit C = C1 Ú A Ú ¬ A. Tout résolvant entre C et
C' de formule de coupure différente de A contient à la fois
A et ¬ A, et est donc une tautologie. Les résolutions
portant sur A sont de la forme :
et fournissent donc des clauses subsumées par C' dans les deux
cas.
¤
Comme aucune tautologie n'est la clause vide, et que tout résolvant
d'une tautologie avec une clause est une clauses subsumée et peut
donc être supprimé, il n'est nécessaire de résoudre avec
une tautologie nulle part dans une dérivation minimale.
On peut donc toujours supprimer toutes les tautologies.
Ceci peut aussi se voir en format de coupures, dans la mesure ou le
lemme 3 dit que l'on peut remplacer toute coupure
avec une tautologie par une instance de Ax ou par une instance de
W. On peut alors rejouer les mouvements de preuves correspondants
présentés en section 1.
Pour les clauses pures, c'est encore plus simple :
Lemme 4
Tout résolvant d'une clause pure avec n'importe quelle clause est
pure.
Preuve : Toute résolution 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.
¤
Encore une fois, aucune clause pure n'est vide, et on peut donc les
supprimer.