TD 3 : Stratégie de résolution et déduction naturelle

Énoncé

EX 1

1.

E = \lbrace ¬P∨¬Q, P∨Q, P∨¬Q, ¬P∨Q \rbrace

Montrons que $E \vdash_¬ \bot$.

$¬P∨¬Q$ $P∨¬Q$    
  $¬Q$   $¬P∨Q$
    $¬P$  

et

$¬P$ $P∨Q$
  $Q$

d’où, enfin :

$¬Q$ $Q$
  $\bot$

3.

C’est l’ordre lexicographique, si à chaque interprétation partielle $I$ telle que $Dom(I) = \lbrace P_1, ⋯, P_n \rbrace$, on associe le mot

I(P_1) ⋯ I(P_n)

Si $I \not ≤ J$ et $J \not ≤ I$ : alors aucun des deux mots $I(P_1) ⋯ I(P_n)$ et $J(P_1) ⋯ J(P_m)$ n’est préfixe de l’autre, donc :

$I(P_1) ⋯ I(P_n) <_{lex} J(P_1) ⋯ J(P_m)$

OU

$J(P_1) ⋯ J(P_n) <_{lex} I(P_1) ⋯ I(P_m)$

4.

Il suffit de montrer qu’il existe une interprétation partielle qui soit un noeud d’échec et qui ne falsifie pas de clause négative de $E$ : le cas échéant, on prendra le maximum pour $≤_{lex}$, lequel existe puisque

  • l’arbre est fini
  • et par 3), deux noeuds d’échecs correspondant à des interprétations $I$ et $J$ sont pas dans la même branche, donc $I \not≤ J$ et $J \not ≤ I$, d’où $I$ et $J$ sont comparables pour $≤_{lex}$

Or, l’interprétation $I_0$ associée à la branche la plus à gauche (à gauche : 0, à droite : 1) de l’arbre ne falsifie aucune clause négative. CQFD.

NB : De manière plus générale, pour tout noeud interne d’interprétation partielle $I$ ayant pour fils gauche $I_0$, toutes les clauses falsifiées par $I_0$ sont nécessairement de la forme :

P_{n+1}∨C'

et ne peuvent donc pas être négatives.

5.

Soit $E$ un ensemble de clauses insatisfiable.

ABS : Supposons que

\bot ∉ E^\ast

Dans $A(E^\ast)$, soit $I$ un noeud d’échec maximal pour $≤_{lex}.

Soit $C$ une clause falsifiée par $I$ ($I \not\vDash C$) et qui a un nombre minimal ($≥1$) de littéraux positifs.

C ≝ P_i ∨ C'

(car il y a au moins un littéral positif $P_i$, d’où $I(P_i)=0$)

Soit

J ≝ I_{\mid \lbrace P_1, ⋯, P_{i-1} \rbrace}
  • Mq $J_1 = J + (P_i \mapsto 1)$ est un noeud d’échec :

    Sinon : On note $I’$ un noeud d’échec descendant de $J_1$ qui est un fils gauche (un tel noeud existe).

    $I’ ≥_{lex} I$ et $I’$ ne falsifie aucune clause négative : absurde.

Donc J_1 \not\vDash C'' où $C’’ ≝ ¬P_i ∨C’’’$ est négative.

Donc par résolution négative :

C'∨C'''∈E^\ast

Or, montrons que $I \not\vDash C’∨C’’’$ (on aura une contradiction, puisque $C’∨C’’’$ a strictement moins de littéraux positifs que $C$) :

  • D’une part : $I \not\vDash C$ donc $I \not\vDash C’$

  • $J_1 \not\vDash C’’’$ donc $J \not\vDash C’’’$, donc $I \not\vDash C’’’$

Il en résulte que :

I \not\vDash C'∨C'''

⟶ absurde.

EX 2

1.

E = \lbrace ¬P∨¬Q, P∨Q, P∨¬Q, ¬P∨Q \rbrace

Montrons que $E \not\vdash_¬ \bot$.

Clairement :

E^\ast = E ∪ \lbrace P, ¬P, Q, ¬Q, P∨P, ¬P∨¬P, Q∨Q, ¬Q∨¬Q \rbrace \not\ni \bot

2.

La stabilité par factorisation et résolution est claire, puisque que tous les littéraux de la clause dérivée sont des littéraux des prémisses.

3.

$𝜋_1$ $𝜋_2$
$P∨C_1$ $¬P∨C_2$
$C = C_1 ∨ C_2$  
$𝜋_1$
$L∨L∨C’$
$L∨C’$

Récurrence sur la dernière règle utilisée dans la preuve $𝜋$ :

  • Initialisation si $(N(𝜋), H(𝜋)) = (1,0)$ : immédiat.

  • Hérédité :

EX 3

Implication Introduction :

$𝛤, 𝜑 \vdash 𝜓$
$𝛤 \vdash 𝜑 ⟹ 𝜓$

Implication Élimination :

$𝛤 \vdash 𝜑 ⟹ 𝜓$ $𝛤 \vdash 𝜑$
$𝛤 \vdash 𝜓$  

$𝜑 \vdash ¬¬𝜑$

$𝜑, ¬𝜑 \vdash 𝜑$ $𝜑, ¬𝜑 \vdash ¬ 𝜑$ Ax
  $𝜑, ¬𝜑 \vdash \bot$  
  $𝜑 \vdash ¬¬𝜑$  
  $\vdash 𝜑 ⟶ ¬¬𝜑$  

$¬¬𝜑 \vdash 𝜑$

$¬¬𝜑, ¬𝜑 \vdash ¬𝜑$ $¬¬𝜑, ¬𝜑 \vdash ¬¬𝜑$ Ax
  $¬¬𝜑, ¬𝜑 \vdash \bot$  
  $¬¬𝜑 \vdash 𝜑$  
  $\vdash ¬¬𝜑 ⟶ 𝜑$  

Leave a Comment