LE GUIDE DES BONNES RÉSOLUTIONS
1 Forme clausale
Un littéral est une formule de la forme p ou ¬p, avec p une variable propositionnelle. Une
clause est une disjonction de littéraux. Une formule φ en Forme Normale Conjonctive
(FNC) est une conjonction de clauses, donc de la forme
φ = (l1,1 ∨ · · · ∨ l1,m1 ) ∧ · · · ∧ (ln,1 ∨ · · · ∨ ln,mn )
| {z } | {z }
clause clause
où chaque li,j est un littéral.
Théorème 1. Pour toute formule ψ, il existe une formule φ en FNC qui est équivalente à ψ.
Démonstration. La procédure suivante permet de convertir n’importe quelle formule en FNC :
1. Éliminer les connecteurs autres que → et ↔ en utilisant les équivalences classiques :
A→B ¬A ∨ B
A↔B (¬A ∨ B) ∧ (¬B ∨ A)
ou bien A↔B (A ∧ B) ∨ (¬A ∧ ¬B)
2. Tirer les négations vers le bas autant que possible, et éliminer les doubles négations :
¬(A ∧ B) ¬A ∨ ¬B
¬(A ∨ B) ¬A ∧ ¬B
¬¬A A
3. Distribuer ∨ sur ∧ :
A ∨ (B ∧ C) (A ∨ B) ∧ (A ∨ C)
4. Éliminer > et ⊥ :
¬> ⊥
¬⊥ >
A∨> >
A∨⊥ A
A∧> A
A∧⊥ ⊥
1
Une clause l1 ∨ · · · ∨ lm peut aussi être représentée par l’ensemble {l1 , . . . , lm }. La clause vide
⊥ est dénotée par {}. Une formule en FNC
φ = (l1,1 ∨ · · · ∨ l1,m1 ) ∧ · · · ∧ (ln,1 ∨ · · · ∨ ln,mn )
peut alors être représentée par l’ensemble de clauses sous-jacentes
E = {{l1,1 , . . . , l1,m1 }, . . . , {l1,n , . . . , l1,mn }}
appelé forme clausale de φ.
2 Résolution
Étant données deux clauses de la forme C = {l1 , . . . , ln , p} et C 0 = {l10 , . . . , ln0 , ¬p}, on définit
la résolvante de C et C 0 par
res(C, C 0 ) = {l1 , . . . , ln , l10 , . . . , ln0 }.
La règle de résolution dit :
De C et C 0 , déduire res(C, C 0 ).
Étant donné un ensemble E de clauses, on dénote par satur(E) l’ensemble saturé de clauses
obtenu par résolutions successives à partir de E.
Théorème 2 (Correction et complétude de la résolution). L’ensemble E est satisfiable si et
seulement si {} ∈
/ satur(E).
Exemple 1. Considérons la formule φ = (p ∨ q) ∧ ¬q ∧ (¬p ∨ ¬r), à laquelle correspond la forme
clausale E = {{p, q}, {¬q}, {¬p, ¬r}}. On regarde toutes les résolutions que l’on peut obtenir à
partir de E :
{p, q} {¬q} {¬p, ¬r}
{p} {q, ¬r}
{¬r}
Donc satur(E) = {{p, q}, {¬q}, {¬p, ¬r}, {p}, {q, ¬r}, {¬r}}. Comme {} ∈
/ satur(E) on en déduit
que E (et donc φ) est satisfiable.
On dit qu’une clause C subsume une clause C 0 si C ⊆ C 0 , auquel cas C 0 est conséquence
logique de C ; en d’autres termes C est “plus précise” que C 0 . Si C, C 0 ∈ E et C subsume C 0 , alors
C 0 peut être retirée de E sans que cela ne change le caractère satisfiable (ou non) de E. Il en
résulte un nouvel ensemble de clauses E 0 plus petit, et donc plus simple à étudier.
2
3 Application : vérifier la validité d’un jugement
Soit φ une formule dont on veut vérifier la validité. On peut voir que
φ est valide si et seulement si ¬φ est insatisfiable.
Cette observation combinée au théorème 2 aboutit à la procédure suivante :
1. Convertir ¬φ en FNC.
2. Construire l’ensemble E de clauses associée.
3. Calculer satur(E).
4. Si {} ∈ satur(E), on en déduit que φ est valide.
Si {} ∈
/ satur(E), alors φ n’est pas valide.
Plus généralement, étant donné un ensemble d’hypothèses {H1 , . . . , Hn } et une conclusion C,
on a
{H1 , . . . , Hn } C si et seulement si H1 ∧ · · · ∧ Hn ∧ ¬C est insatisfiable.
Pour vérifier la validité du jugement {H1 , . . . , Hn } C, on applique donc la procédure suivante :
1. Convertir H1 ∧ · · · ∧ Hn ∧ ¬C en FNC.
2. Construire l’ensemble E de clauses associée.
3. Calculer satur(E).
4. Si {} ∈ satur(E), on en déduit que {H1 , . . . , Hn } C.
Si {} ∈
/ satur(E), alors {H1 , . . . , Hn } 2 C.
Exemple 2. Considérons le jugement {p → (q ∨ ¬r), ¬q, r ∨ ¬p} ¬p. Après mise en FNC on
obtient l’ensemble E = {{¬p, q, ¬r}, {¬q}, {r, ¬p}, {p}}. À partir de E on peut alors dériver la
clause vide comme suit :
{¬p, q, ¬r} {¬q} {r, ¬p} {p}
{¬p, ¬r} {r}
{¬p}
{}
Par conséquent le jugement {p → (q ∨ ¬r), ¬q, r ∨ ¬p} ¬p est valide.