Logique formelle

Chapitre 4

La méthode de résolution
de Robinson

1- Méthode de résolution close

2- Unification
3- Méthode de résolution avec variables
4- Stratégies de résolution

ENSI Logique formelle 1

 La méthode de résolution
• La résolution est une méthode purement syntaxique et
automatisable qui fut mise au point en 1965 par Robinson
• Elle produit des preuves par réfutation similaire au processus
de démonstration par contradiction (ou l'absurde) : ” pour
prouver la validité d’une formule, on démontre l’insatisfiabilité
de sa négation (on suppose que la négation est vraie et on
essaye d'obtenir une contradiction)”
• Grâce à sa simplicité, à son efficacité et à ses propriétés de
complétude, la résolution est le meilleur choix pour faire des
preuves automatiques
• C’est sur cette méthode que repose le principe du langage de
programmation logique Prolog, inventé à Marseille en 1972
• La simplicité est obtenue en appliquant seulement une ou
deux règles d'inférence sur des formules sous forme clausale
ENSI Logique formelle 2
 La méthode de résolution

1- Résolution close (sans variable)

Définition
Soient
• C’ et C’’ deux clauses closes (ou d’ordre 0)
• p un atome
On appelle clause résolvante des clauses C’  p et C’’   p
la clause C’  C’’

Exemple
La résolvante des clauses  p  q  r et  q  t est la
la clause  p  r  t

ENSI Logique formelle 3

 La méthode de résolution

Définition
Soient C’ une clause close (ou d’ordre 0) et l un littéral
(atome ou négation d’atome)

On appelle clause facteur de C’  l  l la clause C’  l

Exemple
• La clause facteur de q  p  q est la clause q  p
• La clause facteur de  p  q   p est la clause  p  q

ENSI Logique formelle 4

 La méthode de résolution
Nous allons présenter la méthode de résolution close (sans
variable) sous forme de système d’inférence (noté R0 )

Le système d’inférence R0 pour la résolution close est

défini par :

 R0 = R 0 U {  ,  } U { F,V } U {}

 FR0 = { clauses d’ordre 0 construites sur R0 }

 AR0 = Ø (aucun axiome)

suite

ENSI Logique formelle 5

 La méthode de résolution
 R R0 (règles d’inférence)
- résolution C’  p C’’   p Res
C’  C’’

- factorisation C  l  l Fact
C l

ENSI Logique formelle 6

 La méthode de résolution
 R R0 (règles d’inférence)
- résolution C’  p C’’   p Res
C’  C’’

- factorisation C  l  l Fact
C l
Cas particulier :

p p
Res


Le symbole  représente la clause vide (contradiction)

qui est la conséquence de la déduction de p et de  p
ENSI Logique formelle 7
 La méthode de résolution

Proposition

 Si {C1, C2} Res C alors {C1, C2} ╞ C

autrement dit { C’  p , C’’   p } ╞ C’  C’’

 Si C1 Fact C alors C1 ╞ C

autrement dit { C’  l  l } ╞ C’  l

ENSI Logique formelle 8

 La méthode de résolution

Preuve
 { C’  p , C’’   p } ╞ C’  C’’
Pour toute interprétation I telle que
[C’  p ]I = [C’’   p ]I = V

- si [p]I = V alors [ p ]I = F donc forcément [C’’ ]I = V

et donc [C’  C’’]I = V

- si [p]I = F alors forcément [C’ ]I = V

et donc [C’  C’’]I = V

 { C’  l  l } ╞ C’  l trivial

ENSI Logique formelle 9

 La méthode de résolution
Soit ℰ un ensemble de clauses closes

Proposition Correction
Si il existe une déduction dans R0 de  à partir de ℰ
alors l’ensemble ℰ est insatisfiable

Proposition Complétude
La méthode de résolution close est réfutationnellement complète
c-à-d Si l’ensemble ℰ est insatisfiable alors
il existe une déduction dans R0 de  à partir de ℰ

Corollaire ℰ est insatisfiable ssi ℰ R0



ENSI Logique formelle 10

 La méthode de résolution

Application
Pour montrer qu’un ensemble ℰ de formules closes est
insatisfiable faire :

1. Mettre chacune des formules de l’ensemble ℰ sous forme

clausale. Ω := ℰC

1. Tant que (  ∉ Ω ) faire

- choisir « Ci et Cj ∈ Ω telles que {Ci , Cj } Res C»

Fact
ou « Ci ∈ Ω telle que Ci C»

- Ω := Ω U {C}
ENSI Logique formelle 11
 La méthode de résolution

Exemple

{pq , pq, pq , pq}

Res

q  q q  q
Fact

q q


Graphe (arbre) de déduction (dérivation)
ENSI Logique formelle 12
 La méthode de résolution

Exemple (suite) {pq , pq, pq , pq}

Autre présentation

pq pq pq pq

Res
qq qq
Fact
q q
Res


ENSI Logique formelle 13

 La méthode de résolution
Ceci donne la déduction suivante :
pq , pq, pq , pq hypothèses
B1 : pq hypothèse
B2 :  p  q «
B3 : qq application de Res à B1 et B2
B4 : q application de Fact à B3
B5 : p   q hypothèse
B6 :  p   q «
B7 :  q   q application de Res à B5 et B6
B8 : q application de Fact à B7
B9 :  application de Res à B4 et B8 stop
ENSI Logique formelle 14
 La méthode de résolution
Remarques
• La règle de factorisation (Fact) est nécessaire. Mais on peut
ne pas l’utiliser explicitement en simplifiant
systématiquement les littéraux redondants dans les clauses
• Lors de la résolution
– on n’est pas obligé d’utiliser toutes les clauses
– on peut utiliser une même clause plusieurs fois
• La règle de résolution (Res) est aussi appelée règle de
coupure (cut). Et la règle de factorisation (Fact) est aussi
appelée règle de diminution
• La règle de résolution généralise la règle du modus ponens
p  B p pB p
M.P Res
B B
ENSI Logique formelle 15
 La méthode de résolution
Exemple
H1 : «si je travaille bien alors je vais réussir»
H2 : «si je suis malade , je ne peux pas bien travailler»
H3 : «je suis malade mais je travaille bien»
C : «je vais réussir»
 montrons que {H1, H2, H3} ╞ C

{H1, H2, H3} ╞ C ssi {H1, H2, H3,  C } est insatisfiable (théroème
de réfutation (TD1Ex3(a))

montrons que ℰ ={ H1,H2, H3,  C } est insatisfiable

On sait que: ℰ est insatisfiable ssi ℰC (sa forme clasuale) est insatisfiable

ℰC est insatisfiable ssi ℰC ⊢R0  suite

ENSI Logique formelle 16

 La méthode de résolution
1) Modélisation
H1 : «si je travaille bien alors je vais réussir»  tr
H2 : «si je suis malade , je ne peux pas bien travailler»
 mt
H3 : «je suis malade mais je travaille bien»  mt
C : «je vais réussir»  r
ℰ ={ H1,H2, H3,  C }={t  r, m   t, m  t,  r}
2) Transformation de ℰ en forme clausale ℰC

ℰC = {  t  r ,  m   t , m , t ,  r }
suite

ENSI Logique formelle 17

 La méthode de résolution

3) Résolution
{tr , m t , m , t ,r}

r t

 

ENSI Logique formelle 18

 La méthode de résolution
2- Unification

L’unification permet de rendre si possible des expressions

identiques (égales syntaxiquement) en instanciant leurs
variables
Elle est nécessaire pour pouvoir appliquer la méthode de
résolution à des clauses avec variables

ENSI Logique formelle 19

 La méthode de résolution
Définition Substitution

Une substitution (notée  ) est un ensemble fini de la forme

{ x1 ← t 1 , … , x n ← t n }

• chaque xi est une variable

• chaque ti est un terme différent de xi

 Une substitution vide (n = 0) est notée 

 Une substitution est dite close si chaque terme ti est clos

ENSI Logique formelle 20

 La méthode de résolution

Définition
Soient
  = { x1 ← t1, …, xn ← tn } une substitution
• E une expression (terme, formule, ensemble de formules)
E est l’expression obtenue en substituant chacun des
termes ti aux occurrences de chaque variable xi

c-à-d E = E[x1 ← t1, …, xn ← tn ]

E est appelé une instance de l’expression E

ENSI Logique formelle 21

 La méthode de résolution

Exemple

 = { x ← a , y ← f(b), z ← c } E: P(y, x)

E = P(y,x)[x ← a , y ← f(b), z ← c ] = P(f(b),a)

ENSI Logique formelle 22

 La méthode de résolution
Définition
Soient
  = { x1 ← t1, …, xn ← tn } et
  = { y1 ← s1, …, ym ← sm }
La composition des deux substitutions  et  notée .
est la substitution calculée à partir de l’ensemble Δ comme suit :

i) Δ := { x1 ← t1 , … , xn ← tn } \ {xi ← ti : xi = ti }

ii) Δ := Δ U (  \ { yi ← si : yi ← * ∈ Δ } )

iii) . = Δ

ENSI Logique formelle 23

 La méthode de résolution
Exemple
 = { x ← f(y) , y ← z }
 = { x← a , y← b , z ← y }

i) Δ := { x ← f(y) , y ← z } := { x ← f(b) , y ← y }

:= { x ← f(b) }

ii) Δ := { x ← f(b) } U { x ← a , y ← b , z ← y }

:= { x ← f(b) , y ← b , z ← y }

. = { x ← f(b) , y ← b , z ← y }

ENSI Logique formelle 24

 La méthode de résolution

Remarque
La composition des substitutions possède les propriétés
suivantes :
• elle est associative (.). = .(.)
• elle n’est pas commutative . ≠ .
• elle possède un élément neutre (à droite et à gauche)
qui est la substitution vide 
. = . = 

ENSI Logique formelle 25

 La méthode de résolution

Définition
 Une substitution  est dite un unificateur de l’ensemble

d’expressions { E1, … , En } ssi

E1 = … = En
" = " égalité syntaxique

 L’ensemble d’expressions { E1, … , En } est dit unifiable

ssi il existe un unificateur de { E1, … , En }

ENSI Logique formelle 26

 La méthode de résolution

Exemple
Soit l’ensemble de termes suivants :

E = { f(x,g(y)) , f(x,g(h(b))) , f(a,z) }

La substitution  = { x ← a , y ← h(b), z ← g(h(b)) } est un

unificateur de E

-f(x,g(y))  = f(a,g(h(b)))

- f(x,g(h(b)))  = f(a,g(h(b)))

-f(a,z)  = f(a,g(h(b)))

D’où: f(x,g(y))  = f(x,g(h(b)))  = f(a,z)  = f(a,g(h(b)))

ENSI Logique formelle 27
 La méthode de résolution
Remarque Un unificateur n’est pas unique

Par exemple pour les deux termes suivants

A : f(x,b) et B : f(g(y),z)

 1 = {x ← g(y) , z ← b} est un unificateur de A et B

 2 = {x ← g(a) , y ← a , z ← b} est aussi un unificateur
de A et B
 3 = {x ← g(f(a)) , y ← f(a) , z ← b} est encore un
unificateur de A et B
• … suite

ENSI Logique formelle 28

 La méthode de résolution
Remarque (suite)
Nous remarquons que pour tout unificateur i il existe une
substitution i telle que
A 1.i = A i = B i = B 1.i

 1 = {x ← g(y) , z ← b} = {x ← g(y) , z ← b}. = 1.1

 2 = {x ← g(a) , y ← a , z ← b}
= {x ← g(y) , z ← b}.{y ← a} = 1.2
 3 = {x ← g(f(a)) , y ← f(a) , z ← b}
= {x ← g(y) , z ← b}.{y ← f(a)} = 1.3
• …
ENSI Logique formelle 29
 La méthode de résolution
Nous voulons avoir un unificateur « minimal »
« minimal » dans le sens où il ne soit pas lui même une
instance d’autres unificateurs. Un tel unificateur est appelé un
« plus général unificateur » (p.g.u)

Définition
Un unificateur  de l’ensemble d’expressions { E1, … , En }
est dit un plus général unificateur
ssi
pour tout unificateur  de { E1 , … , En } , il existe une
substitution  telle que  = .
ENSI Logique formelle 30
 La méthode de résolution
Algorithme d’unification
Nous allons présenter un algorithme d’unification de deux
expressions.

Nous utiliserons les notations suivantes :

rangE(t) : la position de la sous expression t dans E
racine(t) : le symbole racine de t

Exemple :
A : P(f(x), h(a)) B : P(f(y), z)
rangA(f(x)) = rangB(f(y)) et racine(f(x)) = racine(f(y)) = f
rangA(h(a)) = rangB(z) et racine(h(a)) ≠ racine(z)
ENSI Logique formelle 31
 La méthode de résolution
Unification (A ,B : expressions)
début
 := 
tant que (A  ≠ B ) faire
déterminer t1 et t2 les sous expressions les plus à gauche de
A et B telles que
( rangA(t1) = rangB(t2) ) et ( racine(t1) ≠ racine(t2) )
si (t1 et t2 ne sont pas des variables) \\ clash
ou (t1 ∈ Var(t2) ou t2 ∈ Var(t1)) \\ occurcheck
alors arrêt retourner («échec : A et B non unifiables»)
sinon si t1 = x (une variable) alors  := .{ x ← t2}
si t2 = x (une variable) alors  := .{ x ← t1}
fin tant que
retourner ()
ENSI Logique formelle 32
fin
 La méthode de résolution
Exemple 1 A : P(x, f(x), a) B : P(y, z, u)

A B 
P P


x f a y z u

x
P P
.{x ← y}
y f a y z u =
{x ← y}
y
ENSI Logique formelle 33
 La méthode de résolution
A B 
 
P P
{x ← y}.{z ← f(y)}
y f a y f u =
{x ← y, z ← f(y)}
y y

P P
{x ← y, z ← f(y)}
y f a y f a .{u ← a}
=
y y {x ← y , z ← f(y) ,
u ← a}

ENSI Logique formelle 34

 La méthode de résolution
Exemple 2 A : P(x, f(g(x)), a) B : P(b, y, y)

A B 
 
P
P

a b y y
x f

ENSI Logique formelle 35

 La méthode de résolution
A B 
P P

b f a b y y .{x ← b}
=
g {x ← b}

b
P P

b {x ← b}.{y ← f(g(b))}
b f a f f
=
g g g {x ← b, y ← f(g(b))}

b b b
ENSI Logique formelle 36
 La méthode de résolution

A B 

P P

b f a b f f
échec
g g g (clash)

b b b

ENSI Logique formelle 37

 La méthode de résolution
Exemple 3 A : P(x, f(x)) B : P(f(y), y)

A B 
P P


x f f y

x y

ENSI Logique formelle 38

 La méthode de résolution
A B 
P P

f f f y .{x ← f(y)}
=
y f y {x ← f(y)}

y
P P

f f f y échec
(occurcheck)
y f y

y
ENSI Logique formelle 39
 La méthode de résolution

Proposition

L’algorithme d’unification présenté termine et est correct

Autrement dit

Soient A et B deux expressions

L’algorithme d’unification présenté termine
- avec « échec » si A et B ne sont pas unifiables
- en donnant un p.g.u de A et B si A et B sont unifiables

ENSI Logique formelle 40

 La méthode de résolution

Pour calculer le p.g.u d’un ensemble d’expressions

{E1, … , En}, il faut appliquer (n-1) fois l’algorithme précédent en
calculant à chaque itération i une substitution i comme suit :

1. appliquer 1…i-1 à Ei et Ei+1

2. calculer i p.g.u de Ei1…i-1 et Ei+11…i-1

(Ei1 …i-1) i = (Ei+11…i-1) i

L’unificateur de {E1, … , En} est 1…n-2.n-1

suite

ENSI Logique formelle 41

 La méthode de résolution
E1 , E2 , E3 …... Ei , Ei+1 ...... En-1 , En

E 21 , E31 …... Ei1 , Ei+11 ...... En-11 , En1

E 312 … Ei 12 , Ei-112 ... En-112 , En12

…...
Ei12…i-1 , Ei+112…i-1 ...… En12…i-1

Ei+112…i-1i …... En12…i-1i

………
En-11 2…i-1i…n-2 , En 1 2…i-1i…n-2

En12…i-1i…n-2n-1

suite
L’unificateur de {E1, … , En} est 12…i-1i…n-2n-1
ENSI Logique formelle 42
 La méthode de résolution

Exemple
{ P(x,y) , P(f(z),x) , P(u,f(x)) }

1. P(x,y)1 = P(f(z),x)1 = P(f(z), f(z))

1 = { x ← f(z) , y ← f(z) }

2. P(f(z), f(z))2 = (P(u,f(x))1) 2

= P(u, f(f(z)) 2 ( occurcheck)

échec l’ensemble n’est pas unifiable

ENSI Logique formelle 43

 La méthode de résolution
3- Résolution avec variables

Le système d’inférence (noté R1 ) pour la méthode de

résolution devient :

 R1 = R U F U X U {  ,  } U { F, V } U { , } U {}

 FR1 = { clauses du 1er ordre construites sur R1 }

 AR1 = Ø (aucun axiome)

suite

ENSI Logique formelle 44

 La méthode de résolution
R R1 (règles d’inférence)
- résolution C’  A’ C’’   A’’ Res
C’  C’’ 
A’ et A’’ des atomes et  p.g.u de A’ et A’’ (A’ = A’’)

- factorisation C  l’  l’’ Fact

C   l’
l’ et l’’ des littéraux et  p.g.u de l’ et l’’ (l’ = l’’)

 Il faut que deux clauses différentes

n’aient pas de variables communes ► renommage

Cas particulier : A’  A’’ si A’ = A’’

Res

ENSI Logique formelle 45
 La méthode de résolution

Remarque
Il ne faut pas que les clauses aient des variables communes

 Il faut utiliser le renommage

Par exemple {P(x) , Q(x)} veut dire  x P(x)   x Q(x)

or  x P(x)   x Q(x) ≡  x P(x)   y Q(y)

ce qui veut dire {P(x) , Q(y)}

donc {P(x) , Q(x)} ≡ {P(x) , Q(y)}

ENSI Logique formelle 46

 La méthode de résolution
Exemple
 P(x)  Q(x)  P(a)  R(x)
renommage

P(x)  Q(x)  P(a)  R(y)

Res
Q(a)  R(y)
avec ={x←a}

 P(x)  P(f(y))   Q(x)

Fact
P(f(y))   Q(f(y))
avec  = { x ← f(y)}

ENSI Logique formelle 47

 La méthode de résolution

Proposition

 Si { C1 , C2 } Res C alors { C1 , C2 } ╞ C

autrement dit { C’  l’ , C’’   l’’ } ╞ C’  C’’

avec  p.g.u de l’ et l’’

 Si C1 Fact C alors C1 ╞ C

autrement dit { C’  l’  l’’ } ╞ C’  l’

avec  p.g.u de l’ et l’’
ENSI Logique formelle 48
 La méthode de résolution
Preuve
 { C’  l’ , C’’   l’’ }╞ C’  C’’ avec  p.g.u de l’ et l’’

Soit I une interprétation telle que [C’  l’ ]I = [C’’   l’’ ]I = V

alors pour tout , [C’   l’  ]I = [C’’    l’’  ]I = V
en particulier si l’ = l’’, alors
- si [l’]I = V alors [ l’’ ]I = F
donc forcément [C’’]I = V et donc [C’  C’’]I = V
- si [l’]I = F alors forcément [C’]I = V
et donc [C’  C’’]I = V
 { C’  l’  l’’ } ╞ C’  l’ avec  p.g.u de l’ et l’’
même principe
ENSI Logique formelle 49
 La méthode de résolution

Théorème Robinson
La méthode de résolution avec variables est correcte et est
réfutationnellement complète

c-a-d Soit ℰ un ensemble de clauses

ℰ est insatisfiable ssi ℰ R1 

ENSI Logique formelle 50

 La méthode de résolution
Application
Pour montrer qu’un ensemble ℰ de formules de 1er ordre est
insatisfiable faire :
1. Mettre chacune des formules de l’ensemble ℰ sous forme
clausale. Ω := ℰC
2. Renommer les variables des différentes clauses de Ω
3. Tant que (  ∉ Ω ) faire

- choisir « Ci et Cj ∈ Ω telles que {Ci , Cj } Res C»

Fact
ou « Ci ∈ Ω telle que Ci C»
- Ω := Ω U {C}
ENSI Logique formelle 51
 La méthode de résolution
Exemple
{ P(x)  P(f(x)) , P(a) ,  P(f(x)) }

Renommage {  P(x)  P(f(x)) , P(a) ,  P(f(y)) }

{x ← a}

P(f(a))
{y ← a}

Graphe (arbre) de déduction (dérivation)

ENSI Logique formelle 52

 La méthode de résolution

Exemple (suite) { P(x)  P(f(x)) , P(a) ,  P(f(y)) }

Autre présentation

 P(x)  P(f(x)) P(a)

{x ← a}
P(f(a))  P(f(y))
{y ← a}


ENSI Logique formelle 53

 La méthode de résolution
Exemple
H1 : «Tout animal à plumes est un oiseau »
 x P(x)  O(x)
H2 : «Aucun mammifère n’est un oiseau »
 x M(x)   O(x)
C : «Donc, aucun mammifère n’a de plumes »
 x M(x)   P(x)
 montrons que {H1, H2} ╞ C

montrons que { H1 , H2 ,  C } est insatisfiable

{x P(x)  O(x) , x M(x)   O(x) ,  x M(x)  P(x)}
suite

ENSI Logique formelle 54

 La méthode de résolution
1. Forme clausale
{  P(x)  O(x) ,  M(x)   O(x) , M(a) , P(a) }

2. Renommage
{  P(x)  O(x) ,  M(y)   O(y) , M(a) , P(a) }

3. Résolution
{  P(x)  O(x) ,  M(y)   O(y) , M(a) , P(a) }
{y ← a}
{x ← a}  O(a)

 P(a)


ENSI Logique formelle 55
 La méthode de résolution

4- Stratégie de résolution

La méthode résolution de Robinson présentée est non

déterministe à cause du choix des clauses sur lesquelles il faut
appliquer les règles Res et Fact
Le fait d’ajouter une stratégie pour appliquer les règles risque de
rendre la méthode non complète et le fait d’appliquer les règles
d’une façon non déterministe risque aussi de ne pas trouver
facilement la  si elle existe
Nous voulons donc avoir une stratégie qui garde la méthode de
résolution complète et qui nous permet de trouver facilement la
 si elle existe
ENSI Logique formelle 56
 La méthode de résolution

Soit ℰ un ensemble de clauses qu’ont veut montrer insatisfiable

On appellera les clauses de ℰ
les clauses initiales ou clauses input

Définition
Une stratégie de résolution est dite complète si lorsque
l’ensemble ℰ est insatisfiable, alors on est sûre de trouver la 

ENSI Logique formelle 57

 La méthode de résolution
Différentes stratégies possibles
 Une stratégie est dite linéaire si à chaque fois qu’on applique
la règle Res (ou Fact) , une des deux clauses parentes est la
dernière clause résolvante (ou facteur) obtenue

 la stratégie linéaire est une stratégie complète

 Une stratégie est dite linéaire input si elle est linéaire et à

chaque fois qu’on applique la règle Res , une des deux clauses
parentes appartient à l’ensemble des clauses initiales
(clauses input)
 la stratégie linéaire input n’est pas une stratégie complète
suite
ENSI Logique formelle 58
 La méthode de résolution

C’ C’’ C’ , C’’ ∈ ℰ
Res
D1 B1
......

Dk Bk
......

• stratégie linéaire Bk ∈ ℰ U {D1 , ... , Dk-1}

• stratégie linéaire input Bk ∈ ℰ

ENSI Logique formelle 59
 La méthode de résolution
Exemple
{ p  q ,p q , p q ,p q}

q  q q q

q q

 stratégie non linéaire

ENSI Logique formelle 60

 La méthode de résolution
Exemple
{ p  q ,p q , p q ,p q}

q  q

p
 mais non input  il est facile de vérifier
qu’une stratégie linéaire
 stratégie linéaire q
input ne va pas donner
le  (boucle)

ENSI Logique formelle 61
 La méthode de résolution
Exemple

{ p , p  q , qr ,r }

 stratégie linéaire input

ENSI Logique formelle 62

 La méthode de résolution

On appelle littéral positif (qu’on notera l+ ) un atome (sans le

symbole  ) et un littéral négatif (qu’on notera l- ) une négation
d’atome

 Une stratégie est dite négative (resp. positive) si à chaque

fois qu’on applique la règle Res , une des deux clauses
parentes est une clause négative (resp. positive) c-à-d ne
contenant que des littéraux négatifs (resp. positifs)

 les stratégies négatives sont des stratégies complètes.

De même les stratégies positives

ENSI Logique formelle 63

 La méthode de résolution

 Une stratégie est dite ordonnée si les littéraux de chaque

clause sont ordonnés et la règle de résolution (coupure) n’est
permise que sur certains littéraux

Exemple : les littéraux de chaque clause sont ordonnés en

mettant les littéraux positifs en tête. La coupure n’est permise
que sur le littéral situé en tête de chaque clause parente

 une stratégie à la fois linéaire et ordonnée est une

stratégie complète

ENSI Logique formelle 64

 La méthode de résolution

La stratégie SLD
SLD Resolution ( Selected Lineary Defined )

La SLD Resolution est une stratégie :

• linéaire input
• négative
• ordonnée sur les littéraux comme suit :
- les littéraux de chaque clauses sont ordonnés en
plaçant les littéraux positifs en tête
- la coupure n’est autorisée que sur le premier littéral de
chaque clause suite

ENSI Logique formelle 65

 La méthode de résolution

C B0 C, B0 , ... , Bk ∈ ℰ
Res
D1 B1 C négative
...... D1 , ... , Dk négatives
Dk Bk
......

 chaque clause résolvante Di est forcément une clause

négative de la forme  A  l-1  ...  l-n (A un atome)

 à chaque itération i , on choisit une clause Bi ∈ ℰ de la

forme A’  l’1  ...  l’m telle que il existe  p.g.u de
A et A’ et on applique la règle Res (on dit on coupe sur
les premiers littéraux de tête)
ENSI Logique formelle 66
 La méthode de résolution
Remarques
 La stratégie SLD est en général non complète car elle est
input. Elle devient complète si les clauses initiales sont des
clauses de Horn . C’est le principe du langage Prolog
 Une clause de Horn est une clause contenant au plus un
littéral positif
 On doit au moins avoir une clause initiale complètement
négative pour pouvoir initialiser la SLD Resolution
 En adoptant la stratégie SLD, la règle de factorisation (Fact)
n’est plus nécessaire
 Une stratégie SLD peut nous aider à savoir si un ensemble de
clauses est éventuellement satisfiable (mais pas
systématiquement)
ENSI Logique formelle 67
 La méthode de résolution
Mise en œuvre de la SLD Resolution
• l’ensemble des clauses initiales est ordonné comme suit :
ℰ = { C-1 , ... , C-n , C1+1 , ... , C1+m , l+1 , ... , l+p }

C-i : clauses négatives

C1+j : clauses de Horn avec un seul littéral positif
le littéral positif est placé en tête
l+k : clauses unitaires positives (un seul littéral positif)
• au départ : application de la règle Res sur une clause négative
( C-i ) avec clause contenant un littéral positif ( C1+j ou l+k )
• à chaque itération : application de la règle Res sur la dernière
résolvante obtenue avec une clause contenant un littéral positif
( C1+j ou l+k )
ENSI Logique formelle 68
 La méthode de résolution
Exemple SLD resolution
{p q , q r , p s ,r , s }

q  s

r  s

s


ENSI Logique formelle 69
 La méthode de résolution
Exemple
{p  q ,q r , p s ,r , s }

p  r

p

 n’est pas une stratégie SLD

car ordre non respecté s
 La coupure ne s’est pas faite
sur les têtes des clauses
 mais stratégie linéaire input 
ENSI Logique formelle 70
 La méthode de résolution
Conclusion
Pour montrer qu’un ensemble de clauses ℰ est insatisfiable par la
méthode de résolution, on peut adopter la démarche suivante:
• ordonnée l’ensemble ℰ comme suit :
{ C-1 , ... , C-n0 , C1+1 , ... , C1+n1 , C2+1 , ... , C2+n2 ,
... , Cp+1 , ... , Cp+np , l+1 , ... , l+m }

C-i0 : clauses négatives

C1+i1 : clauses avec 1 littéral positif placé en tête
C2+i2 : clauses avec 2 littéraux positifs placés en tête
...
Cp+ip : clauses avec p littéraux positifs placés en tête
suite
l+k : clauses unitaires positives
ENSI Logique formelle 71
 La méthode de résolution
• si toutes les clauses sont négatives
(n0 ≥ 1 , n1 = n2 = ...= np = m = 0)
 l’ensemble ℰ n’est pas insatisfiable
de même si toutes les clauses sont positives

• si ℰ contient au moins une clause négative, au moins une

clause positive unitaire et les autres clauses sont des clauses
de Horn avec un littéral positif
(n0 ≥ 1, n1 ≥ 1 , n2 = ...= np = 0 , m ≥ 1)
 appliquer la SLD résolution

• si non utiliser une autre stratégie : linéaire négative ou

positive (mais pas input)
ENSI Logique formelle 72