Cours 2 : Complétude et Complétude réfutationnelle

Complétude

$I$ est complet :

si $\vDash ⊆ \vdash_I$

Complétude de la résolution

Complétude réfutationnelle :

si $H$ est insatisfaisable, alors $H \vdash_I \bot$

Th : Res+Fact est réfutationnellement complet.

Soit $H$ un ensemble de clauses.

\[H^\ast ≝ \lbrace C \mid H \vdash_I C \rbrace\] \[\bot ∈ H^\ast \text{ ssi } A(H^\ast) \text{ vide }\]

Par l’abs, supposons que :

  • $H$ est insatisfaisable
  • $A(H^\ast)$ est non vide

$H$ insatisfaisable ssi $A(H)$ est fini

$H$ insat. ssi $H^\ast$ insat :

  • $⟹$ : car $H ⊆ H^\ast$
  • $⟸$ : car si $I \vDash H$, alors $I \vDash H^\ast$ par correction du système d’inférence

Par l’absurde, supposons qu’on puisse avoir :

  • $A(H^\ast)$ est fini

et

  • $A(H^\ast)$ est non vide

Il existe dans l’arbre $A(H^\ast)$ un noeud $I_0$ dont les deux fils $I_1$ et $I_2$ sont des noeuds d’échec.

d’où :

  • $I_0$ ne falsifie aucune clause de $H^\ast$
  • il existe une clause $C_1∈H^\ast$ (resp. $C_2∈H^\ast$) tq $I_1$ (resp. $I_2$) falsifie $C_1$ (resp. $C_2$)

Soit

\[\lbrace P_1, ⋯, P_{n-1} \rbrace = Dom_(I_0)\]
  • $I_1$ : $I_0$ étendu par $P_n \mapsto 0$
  • $I_2$ : $I_0$ étendu par $P_n \mapsto 1$

Alors : $P_n$ (ou $\lnot P_n$) est un littéral de $C_1$ car $C_1$ n’est pas falsifié par $I_0$.

Mais ça ne peut pas être $\lnot P_n$, puisque c’est $P_n \mapsto 0$ qui falsifie $C_1$.

Idem pour $C_2$.

Donc :

  • $C_1 = P_n ∨ C’_1$
  • $C_2 = \lnot P_n ∨ C’_2$

Donc par la règle (Res), on peut dériver $C’_1 ∨ C’_2$ de $C_1$ et $C_2$, et

\[C'_1 ∨ C'_2∈H^\ast\]

Quitte à supposer $C’_1$ et $C’_2$ minimales, on a par factorisation :

  • $P_n \not∈ VarProp(C’_1)$
  • $P_n \not∈ VarProp(C’_2)$

Donc :

$I_1$ falsifie $C_1$, d’où $I_1$ falsifie $C’_1$, donc $I_0$ falsifie $C’_1 \not\ni P_n$

De même, $I_0$ falsifie $C’_2$

Donc $I_0$ falsifie $C’_1 ∨ C’_2∈H^\ast$ : absurde, puisque $I_0$ n’est pas un noeud d’échec.

On peut même restreindre les règles, et garder le caractère réfutationnellement complet :

1. Stratégie ordonnée (Res max)

(Res) seulement si $P$ est maximale dans $C∨P$ et dans $C∨ \lnot P$

2. Stratégie négative

(Res) seulement si $C’$ ou $C$ ne contient que des littéraux négatifs.

3. Stratégie unitaire

Une des deux prémisses est réduite à 1 littéral.

PAS réf. complet !

⟶ Réf. complet pour les clauses de Horn

Clauses de Horn :

au plus un littéral positif par clause

3. Stratégie linéaire

L’arbre de preuve est un peigne : chaque noeud a au plus un fils qui n’est pas une hypothèse.

PAS réf. complet !

⟶ Réf. complet pour les clauses de Horn

3. Stratégie de sélection

On a une fonction de sélection qui sélectionne un littéral de la clause :

\[f: clause ⟶ \text{ un littéral de la clause}\]
$C∨\lnot P$ $C’∨ P$
  $C’∨C$

seulement si

  • $P = f(C∨P)$
  • $\lnot P = f(C’∨P)$

PAS réf. complet !

⟶ Réf. complet pour les clauses de Horn

NB : généralise les stratégie négative, unitaire et ordonnée !

Complétude

$S \vDash 𝜑$

ssi

$S, \lnot 𝜑 \vDash \bot$

DONC

$S \vDash L_1 ∨ ⋯ ∨ L_n$

ssi

$S, \lnot L_1, ⋯, \lnot L_n \vDash \bot$

Fact+Res n’est PAS complet

Th : $\lbrace Res, Fact, xx\rbrace$ est complet

$𝜑 = L_1 ∨ ⋯ ∨ L_n$

Si $S \vDash 𝜑$ alors $S, \lnot L_1, ⋯, \lnot L_n \vdash_{Res+Fact} \bot$

Par récurrence sur la preuve de $S, \lnot L \vdash C_0$ :

SI $S, \lnot L \vdash C_0$, ALORS $S \vdash L ∨ C_0$

  • Si la dernière règle est une résolution : $C_0 = C’∨C$
$𝜋_1$ $𝜋_2$
$C∨\lnot P$ $C’∨ P$
  $C’∨C$

Par HR :

$S, \lnot L_0 \vdash C∨\lnot P$ entraîne

\[S \vdash L_0 ∨ C∨\lnot P\]

Puis : symétrie, et règle de factorisation.

  • Si la dernière règle est une factorisation : $C_0 = L∨C$ : on procède de même

PROBLÈME : le cas de base n’est PAS vérifié dans le système d’inférence Res+Fact !

  • Cas de Base : $C_0 ∈ S∪ \lbrace \lnot L_0 \rbrace$

    • Si $C_0 = \lnot L_0$ : on voit bien qu’il faut ajouter la règle du tiers-exclus
    • Si $C_0 = S$ : on voit bien qu’il faut ajouter la règle d’affaiblissement :
$C$
$C∨L$

Il nous faut donc revenir à l’hérédité dans la preuve par récurrence, pour traiter les cas où :

  • La dernière règle est un affaiblissement : $C_0 = C∨L$

    trivial

  • La dernière règle est un tiers-exclus : $C_0 = P∨\lnot P$

    on utilise la règle d’affaiblissement, et le résultat en découle de manière immédiate.

On a donc montré que :

SI $S, \lnot L \vdash C_0$, ALORS $S \vdash L ∨ C_0$

donc avec $C_0=\bot$,

SI $S, \lnot L \vdash \bot$, ALORS $S \vdash L ∨ \bot \vdash L$

Donc avec la complétude réfutationnelle :

Si $S \vDash 𝜑$

alors

$S, \lnot 𝜑 \vDash \bot$ ($S, \lnot 𝜑$ insatisfaisable)

alors (complétude réfutationnelle)

$S, \lnot 𝜑 \vdash \bot$

alors (démonstration précédente, avec $C_0 = \bot$)

$S \vdash 𝜑$

Stratégie de sélection

$C∨P$ $C’∨\lnot P$
$C∨C’$  

seulement si

\[f(C∨P)= P \\ f(C'∨\lnot P) = \lnot P\]

$f: Clauses ⟶ Littéraux$

Ex :

  • Stratégie ordonnée : $f= \max$
  • Stratégie négative : $f$ sélectionne un littéral positif s’il y en a un

Ex : $f$ : sélection arbitraire (littéraux soulignés)

\[\underbrace{P}_{}∨ \lnot Q, \underbrace{Q}_{}\]

⟶ aucune inférence possible

\[\underbrace{P}_{}∨ \lnot Q \\ \underbrace{Q}_{}∨ ¬R \\ \underbrace{¬Q}_{}∨ ¬P\]

⟶ seule inférence possible : $¬R ∨ ¬P$

\[\underbrace{P}_{}∨ \lnot Q \\ \underbrace{Q}_{}∨ ¬R \\ \underbrace{¬R}_{}\]

⟶ aucune inférence possible

Th : Pour toute fonction de sélection, la stratégie de sélection est réfutationnellement complète pour les clauses de Horn.

NB : contre-ex pas avec les clauses de Horn :

\[\underbrace{P}_{}∨ Q \\ \underbrace{Q}_{}∨ ¬P \\ \underbrace{¬Q}_{}∨ P \\ \underbrace{¬P}_{}∨ ¬Q\]

clairement insatisfaisable.

Deux inférences possibles : $P∨¬P, ¬Q∨Q$, puis : plus aucune autre inférence possible, alors qu’il est insatisfaisable ! ⟶ non réf. complet.

Preuve :

On suppose que $E$ est insatisfaisable.

\[E^\ast ≝ \lbrace C \mid E \vdash_f C \rbrace\]

$E^\ast$ est un ensemble de clauses de Horn.

Mq $\bot ∈ E^\ast$

NB : Caractérisation des clauses de Horn : l’intersection de deux modèles est toujours un modèle ⟶ structure de trellis (pour l’inclusion)

Contre-Ex : $P∨Q$ ⟶ les modèles $\lbrace P \rbrace$, $\lbrace Q \rbrace$ ont une intersection qui ne satisfait pas $P∨Q$

DONC : Clauses de Horn ⟹ existence d’un plus petit modèle (un inf pour l’intersection).

Par l’absurde : si $\bot ∉ E^\ast$ :

On pose

\[I_0 ≝ E^\ast ∩ 𝒫\]
  • 1er Cas (particulier, pour fixer les idées) : $f$ sélectionne un littéral négatif quand c’est possible.
\[I_0 \not\vDash E^\ast\]

Soit $C$ une clause de $E^\ast$ falsifiée par $I_0$

  • Cas 1 : soit $C = ¬P_1 ∨ ⋯ ∨ ¬P_n$, alors $P_1, ⋯, P_n ∈ I_0$, et
\[E \vdash_f P_1, ⋯, P_n\]

Récurrence sur $n$ :

Si, sans perte de généralité $P_1$ est sélectionné par $f$, par résolution, on dérive de $P_1$ et $C$ : $¬P_2 ∨ ⋯ ∨ ¬P_n$

on conclut par récurrence descendante.

  • Cas 2 :

$C = P ∨ ¬P_1 ∨ ⋯ ∨ ¬P_n$, alors $P_1, ⋯, P_n ∈ I_0$, et

$f$ ne peut pas sélectionner $P$ (par hypothèse).

Si $n≠0$ : on réduit la formule comme précédemment, sinon si $n=0$ : impossible car $P∈I_0$ et $I_0$ falsifie $P$.

Cas général :

\[I_1 ≝ I_0 ∪ \lbrace P \mid \underbrace{P}_{} ∨ ¬P_1 ∨ ⋯ ∨ ¬P_n ∈ E^\ast, P_1, ⋯, P_n ∈ I_0 \rbrace \\ I_{n+1} ≝ I_n ∪ \lbrace P \mid \underbrace{P}_{} ∨ ¬P_1 ∨ ⋯ ∨ ¬P_n ∈ E^\ast, P_1, ⋯, P_n ∈ I_n \rbrace\] \[I = \bigcup_{n≥0} I_n\]

$I$ falsifie une clause $C∈E^\ast$

$∃n$ minimal tel que $I_n$ falsifie $C$ ($n$ minimal $>0$ (si $n=0$ : on se ramène au cas précédent))

  • Cas 1 : soit $C = ¬P_1 ∨ ⋯ ∨ ¬P_n$, alors $P_1, ⋯, P_n ∈ I_n$, et on conclut par récurrence descendante comme précédemment dans l’exemple que $\bot ∈E^\ast$

  • Cas 2 :

$C = P ∨ ¬P_1 ∨ ⋯ ∨ ¬P_n$ ($C$ minimale) alors $P_1, ⋯, P_n ∈ I_n$, et

$f(C) = P$ par minimalité.

Donc $P ∈ I_{n+1}$ par définition, et, par suite :

$I$ ne falsifie pas $C$ : absurde.

Leave a comment