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 ¬¬𝜑 ⟶ 𝜑$