Previous Next Contents

3  Hyperrésolution

Nous revenons à partir de maintenant à une présentation des dérivations par résolution sous forme d'arbres de preuves par coupures.

Une réfutation par résolution, c'est-à-dire une preuve de la clause vide n'utilisant que la règle Cut à partir de l'ensemble S de clauses, est un objet très malléable que l'on peut déformer à volonté.

L'idée pour améliorer l'efficacité de la recherche de preuve, est de déformer systématiquement les réfutations dans l'espoir d'arriver à un format canonique de réfutation, de même que l'élimination des coupures fournissait les preuves sans coupure comme formes canoniques des preuves de LK0. Ceci mène à chercher des restrictions de la règle de résolution qui préservent la complétude. On les appelle des raffinements de la résolution.

Le premier que nous allons étudier est l'hyperrésolution positive : c'est le raffinement de la résolution où l'une des prémisses de la règle de résolution est contrainte à être une clause positive, c'est-à-dire une clause de la forme A1 Ú ... Ú An (aucune négation). C'est donc la règle :



Intuitivement, une clause positive C est un fait connu, exprimé sous forme de disjonction de faits élémentaires, les atomes. Une clause non positive ¬ A1 Ú ... Ú ¬ Am Ú B1 Ú ... Ú Bn, m³ 1, est alors une règle de déduction A1 Ù ... Ù Am Þ B1 Ú ... Ú Bn. La règle d'hyperrésolution positive exprime alors que l'on peut se contenter de dériver de nouvelles clauses à partir de faits, ce en utilisant les règles, pour aboutir au fait vide. On n'a jamais besoin d'inférer des règles dérivées d'abord purement à partir d'autres règles.

Par exemple, pour montrer que :

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

est insatisfiable, nous nous interdisons de résoudre A Ú ¬ B avec ¬ A Ú ¬ B. Par contre, nous partons du fait AÚ B, et déduisons les nouveaux faits A (par résolution avec A Ú ¬ B sur B), B (avec ¬ A Ú B sur A), ¬ B (par résolution entre le fait A et ¬ A Ú ¬ B), et enfin la clause vide (par résolution entre le fait B et la règle ¬ B).

Pour montrer que cette règle est complète, prenons une réfutation par résolution quelconque, et transformons-la petit à petit en une réfutation par hyperrésolution positive.

Remarquons d'abord :


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


 Preuve : Comme p n'est pas obtenue par hyperrésolution positive, elle contient une coupure entre deux clauses non positives. Choisissons une occurrence minimale d'une telle coupure, c'est-à-dire la plus basse possible dans p :



Comme C1 Ú B n'est pas positive, C1 n'est pas positive et C1 Ú C2 non plus. En particulier, C1 Ú C2 n'est pas la conclusion de p, qui est la clause vide. Donc C1 Ú C2 est nécessairement prémisse d'une coupure dans p. Comme la coupure ci-dessus a été choisie minimale telle que ses deux prémisses soient non positives, C1 Ú C2 est donc nécessairement coupée avec une clause positive dans p. ¤

Nous définissons alors les règles de réécriture suivantes sur les rédex. Il y a trois cas, selon que ¬ A, qui est dans C1 Ú C2, est dans C1 uniquement, dans C2 uniquement, ou dans C1 et C2 en même temps :



où il est sous-entendu que C est une clause positive, que dans la règle (2) C1 n'est pas positive, et que dans toute sous-dérivation notée sous la forme :



les littéraux L1, ..., Lk n'apparaissent pas dans C'.

Si cette relation de réécriture termine, toute forme normale d'une réfutation par résolution est donc une réfutation par hyperrésolution positive à partir du même ensemble S de clauses de départ, par le lemme 5. Il ne reste qu'à montrer que ce système de réécriture termine (faiblement suffirait).

Pour ceci, on traduit les preuves dans un langage du premier ordre de signature fn, n Î N (unaires) et a (constante) par Thyper (C) = a si C est un axiome dans S (une preuve sans prémisse), et sinon :



où n est le nombre de littéraux négatifs (i.e., de la forme ¬ D) dans la clause C.

Notons n1 le nombre de littéraux négatifs de C1, n2 celui de C2, n'1 celui de C'1, n'2 celui de C'2. Remarquons que dans le cas (2) n1 ³ 1, car C1 n'est pas positive : on peut donc poser C1 = C'1 Ú ¬ A' pour un certain A' et choisir n1 = n'1+1. (Ceci permet d'uniformiser la notation de la règle (2) ci-dessous par rapport aux autres.)

Via la traduction Thyper, nous sommes donc ramenés à prouver que le système de réécriture suivant termine :

(1)
f0 (t0, f
 
n'1+1
(t1, t2))
®
f
 
n'1
(f0 (t0, t1), t2)
(2)
f0 (t0, f
 
n'1+1
(t1, t2))
®
f
 
n'1+1
(t1, f0 (t0, t2))
(3)
f0 (t0, f
 
n'1+1
(t1, t2))
®
f
 
n'1
(f0 (t0, t1), f0 (t0, t2))


Lemme 6   Le système de réécriture ci-dessus termine.
Preuve : Nous définissons d'abord une réinterprétation des termes dans les entiers par :
[fn (t1, t2)] = n . [t1] + [t2]      [a] = 1

Nous remarquons que :
  1. (a) pour tout t, [t] > 0 (une récurrence structurelle facile sur t);
  2. (b) [fn'1+1 (t1, t2)] > [t1] (car n'1+1 ³ 1, et [t2] > 0 par (a));
  3. (c) [fn'1+1 (t1, t2)] > [t2] (car n'1+1 ³ 1, et [t1] ³ 1 par (a));
  4. (d) [fn'1+1 (t1, t2)] > [f0 (t0, t2)] pour tout terme t0 (car [f0 (t0, t2)] = [t2], et (c));
  5. (e) Notons Þ la relation de réduction induite par les règles (1)-(3); si t Þ t', alors [t] ³ [t'] (en effet, c'est vrai si t ® t' est l'une des règles, et l'interprétation est monotone : [t1] ³ [t'1] et [t2] ³ [t'2] impliquent [fn (t1, t2)] ³ [fn (t'1, t'2)]);
Soit SN l'ensemble des termes t fortement normalisants, c'est-à-dire tels qu'il n'existe pas de réduction infinie partant de t. Remarquons que pour tout t Î SN, on peut définir la plus grande longueur des réductions partant de t : il n'y a en effet qu'un nombre fini de telles réductions, par le lemme de König, puisque tout terme n'a qu'un nombre fini de réduits (en une étape) possibles. Remarquons que si t Þ t', alors n (t) > n (t'). Nous montrons maintenant que : (f) fn (t0, t) Î SN pour tout n ³ 1 et tous t0, tÎ SN. En effet, toutes les réductions partant de fn (t0, t) prennent place dans t0 ou t, et sont donc finies. Formellement, on démontre (f) par récurrence sur n (t0) + n (t). Soit R une réduction arbitraire partant de fn (t0, t). Si R est vide, elle est trivialement finie. Sinon, R est de la forme fn (t0, t) Þ u suivi d'une réduction R'. Nous avons alors deux cas. Dans le premier cas, u est de la forme fn (t'0, t), avec t0 Þ t'0, donc n (t'0) < n (t0) : nous pouvons donc appliquer l'hypothèse de récurrence et en déduire que R' est finie. Dans le second cas, u est de la forme fn (t0, t') avec t Þ t', donc n (t') < n (t) et encore par hypothèse de récurrence R' est finie. Dans les deux cas, on conclut que R est finie. Comme R est arbitraire, fn (t0, t) Î SN. Ensuite, nous avons : (g) f0 (t0, t) Î SN pour tous t0, tÎ SN. Ceci se démontre de façon similaire à (f), mais cette fois-ci par récurrence sur ([t], n (t0) + n (t)) ordonné lexicographiquement. Allons un peu plus vite : le seul cas qui change est celui où R est non vide, et est donc de la forme f0 (t0, t) Þ u suivi d'une réduction R'. Si u = f0 (t'0, t) avec t0 Þ t'0, R' est finie par récurrence. Si u = f0 (t0, t') avec t Þ t', alors [t'] £ [t] par (e), et n (t0) + n (t') < n (t0) + n (t), donc nous pouvons encore appliquer l'hypothèse de récurrence et conclure que R' est finie. Si u est un rédex, alors t est de la forme fn'1+1 (t1, t2), et nous avons trois sous-cas, correspondant chacun à une règle :
  1. (1) par (b), [t1] < [t], donc nous pouvons appliquer l'hypothèse de récurrence et conclure que : (h.1.a) f0 (t0, t1) Î SN. D'autre part, puisque t = fn'1+1 (t1, t2) Î SN, nous avons aussi : (h.1.b) t2 Î SN. Si n'1 > 0, alors on déduit de (f), (h.1.a) et (h.1.b) que fn'1 (f0 (t0, t1), t2) Î SN, donc que R' est finie. Si n'1 = 0, alors par (c) [t2] < [t], et ceci nous permet de conclure que fn'1 (f0 (t0, t1), t2) Î SN par hypothèse de récurrence, (h.1.a) et (h.1.b), donc encore une fois que R' est finie.
  2. (2) par (c), [t2] < [t], donc nous pouvons appliquer l'hypothèse de récurrence et conclure que f0 (t0, t2) Î SN. Comme t1 Î SN puisque tÎ SN, on en déduit par (f) que fn'1+1 (t1, f0 (t0, t2)) Î SN, donc que R' est finie.
  3. (3) comme ci-dessus, par récurrence nous inférons que : (h.3.a) f0 (t0, t1) Î SN et : (h.3.b) f0 (t0, t2) Î SN. Si n'1 > 0, on en déduit par (f) que fn'1 (f0 (t0, t1), f0 (t0, t2)) est dans SN, et donc que R' est finie. Sinon n'1 = 0, mais par (d) [f0 (t0, t2)] < [fn'1+1 (t1, t2)], donc nous pouvons appliquer l'hypothèse de récurrence encore une fois pour inférer que fn'1 (f0 (t0, t1), f0 (t0, t2)) est dans SN.
Dans tous les cas, R' est finie, donc R aussi. Comme R est arbitraire, il en découle que f0 (t0, t) Î SN. Nous montrons maintenant que t Î SN pour tout t, par récurrence structurelle sur t : si t=a, c'est évident, si t est de la forme fn (t0, t'), c'est une conséquence de (f) si n³ 1 et de (g) si n=0. ¤


Corollaire 7   L'hyperrésolution positive est complète.
Preuve : Soit S un ensemble de clauses insatisfiable. Il existe une réfutation p par résolution de S. Par le lemme 6, p a une forme normale p' pour ®, qui est une réfutation de S. De plus, par le lemme 5, p' est nécessairement une réfutation par hyperrésolution positive. ¤



Previous Next Contents