La méthode de résolution de Robinson

= { x1 ← t1, …, xn ← tn } une substitution

• E une expression (terme, formule, ensemble de formules)

est l’expression obtenue en substituant chacun des est l’expression obtenue en substituant chacun des

Es Es termes ti aux occurrences de chaque variable xi c-à-d Es = E[x1 ← t1, …, xn ← tn ] Es

est appelé une instance de l’expression E

ENSI

Logique Mathématique

19

La méthode de résolution

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

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

ENSI

Logique Mathématique

20

La méthode de résolution

Définition

Soient • s = { x1 ← t1, …, xn ← tn } et • q = { y1 ← s1, …, ym ← sm }

La composition des deux substitutions s et q est la substitution calculée à partir de l’ensemble ∆ comme suit : est la substitution calculée à partir de l’ensemble ∆ comme suit :

notée s

.q

i) ∆ := { x1 ← t1 ii) ∆ := ∆ U ( q

iii)

q = ∆ .q

q , … , xn ← tn

q } \ {xi ← ti

: xi = ti

}

\

{ yi ← si :

yi ← * ∈∈∈∈ ∆ } )

ENSI

Logique Mathématique

21

s s s q q q q q s s s s q q La méthode de résolution

Exemple

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

i) ∆ := { x ← f(y)q

, y ← zq

} := { 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 }

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

ENSI

Logique Mathématique

22

s s La méthode de résolution

Remarque

La composition des substitutions possède les propriétés

suivantes :

.q ).l • elle est associative (s • elle n’est pas commutative s • elle n’est pas commutative s

.(q .l )

= s .q ≠ q .s .q ≠ q .s

• elle possède un élément neutre (à droite et à gauche)

qui est la substitution vide e

.e = e .s

= s

ENSI

Logique Mathématique

23

s La méthode de résolution

Définition (cid:1) Une substitution s

est dite un unificateur de l’ensemble

d’expressions { E1, … , En } ssi

E1

= … = En

" = " égalité syntaxique " = " égalité syntaxique

(cid:1) L’ensemble d’expressions { E1, … , En } est dit unifiable

ssi

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

ENSI

Logique Mathématique

24

s s 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 s = { x ← a , y ← h(b), z ← g(h(b)) } est un

unificateur de E

f(x,g(y)) s

= f(x,g(h(b))) s

= f(a,z) s

= f(a,g(h(b)))

ENSI

Logique Mathématique

25

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)

• s

• s • s

• s

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

• …

ENSI

unificateur de A et B

Logique Mathématique

suite

26

La méthode de résolution

Remarque (suite) Nous remarquons que pour tout unificateur s substitution l telle que 1111....l A s

i = B s

i = A s

i = B s

i

il existe une

i

1111.l

i

• s • s

• s

1 = {x ← g(y) , z ← b} = {x ← g(y) , z ← b}.e = s 2222 = {x ← g(a) , y ← a , z ← b}

1.l

1

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

1111.l

2

1111.l

3

• …

ENSI

Logique Mathématique

27

s s s s s s s s s s s s 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 s

de l’ensemble d’expressions { E1, … , En }

est dit un plus général unificateur

ssi

pour tout unificateur q substitution l

de { E1 , … , En } , il existe une = s telle que q

.l

ENSI

Logique Mathématique

28

s s s s s s s s s s 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 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 Mathématique

29

La méthode de résolution

Unification (A ,B : expressions) début := e

tant que (A s ≠ B s déterminer t1 et t2 les sous expressions les plus à gauche de As et Bs

telles que

) faire

( rangA(t1) = rangB(t2) ) et ( racine(t1) ≠ racine(t2) )

si si

(t1 et t2 ne sont pas des variables) (t et t ne sont pas des variables)

ou (t1

∈∈∈∈ Var(t1)) ∈∈∈∈ Var(t2) ou t2 ∈∈∈∈ ∈∈∈∈

alors arrêt retourner («échec : A et B non unifiables») sinon si t1 = x (une variable) alors s si t2 = x (une variable) alors s

.{ x ← t2} .{ x ← t1}

:= s := s

fin tant que retourner (s fin

ENSI

)

Logique Mathématique

30

s La méthode de résolution

Exemple 1 A : P(x, f(x), a) B : P(y, z, u)

A s P

f

x

P

f

y

x

y

a

a

B s P

y

z

u

P

z

u

y

e .{x ← y} = {x ← y}

ENSI

Logique Mathématique

31

e e e e s e e e La méthode de résolution B s

A s

y

y

P

f

y

P

f

y

a

a

y

y

P

f

y

P

f

y

u

a

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

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

ENSI

Logique Mathématique

32

s La méthode de résolution

Exemple 2 A : P(x, f(g(x)), a) B : P(b, y, y)

B s

P

y y

y y

a

b b

A s

x

P

f f

g

x

ENSI

Logique Mathématique

33

e e e e s La méthode de résolution B s P

A s P

b

b

f

g

b b

P

f

g

b

a

b

y

y

e .{x ← b} = {x ← b}

a

b

P

f

g

b

f

g

b

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

ENSI

Logique Mathématique

34

s e e e La méthode de résolution

b

A s

P

f

g

b

a

b

B s

P

f

g

b

f

g

b

échec échec (clash)

ENSI

Logique Mathématique

35

s La méthode de résolution

Exemple 3 A : P(x, f(x)) B : P(f(y), y)

A s

P

x x

B s

P

y y

f f

x

f f

y

ENSI

Logique Mathématique

36

e e e e s La méthode de résolution B s P

A s P

f

y

f

y

P

f

f

y y

f

f

y

y

y

P

f

y

f

y

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

échec (occurcheck)

ENSI

Logique Mathématique

37

s e e e 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 Mathématique

38

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 s

i comme suit :

1. appliquer s

1…s

i-1 à Ei et Ei+1

2. calculer s 2. calculer s

i p.g.u de Ei i p.g.u de Ei 1 …s

i-1) s

(Ei

1…s 1…s i = (Ei+1

i-1 et Ei+1 i-1 et Ei+1 i-1) s 1…s

1…s 1…s

i-1 i-1

i

L’unificateur de {E1, … , En} est s

1…s

n-2.s

n-1

ENSI

Logique Mathématique

suite

39

s s s s s s s s s s s s s s s La méthode de résolution

E1

, E2

, E3 …... Ei , Ei+1

...... En-1 , En

E2

1 , E3

1 …... Ei

1 , Ei+1

1 ...... En-1

1 , En

1

E3

2 … Ei

1

2 , Ei-1

1

2 , En

1

2

1

1

... En-1

2 …... 2…s …... E s i …... En

i-1

1

Ei

1

2…s

E s Ei+1

1

i-1 , Ei+1 2…s s …s

i-1

...… En 2…s s …s

1

2…s

1

i-1

i-1

i

……… 2…s

i-1

En-1

1

i…s

n-2

, En

1

2…s

i-1

i…s

n-

2

En

1

2…s

i-1

i…s

n-2

n-1

L’unificateur de {E1, … , En} est s

1

2…s

i-1

i…s

n-2

n-1

ENSI

Logique Mathématique

suite

40

s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s La méthode de résolution

Exemple

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

1. P(x,y)s

1 = P(f(z),x)s

1 = P(f(z), f(z))

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

2. P(f(z), f(z))s

2 = (P(u,f(x))s

1) s = P(u, f(f(z)) s

2

2

( occurcheck)

échec l’ensemble n’est pas unifiable

ENSI

Logique Mathématique

41

s s s s 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 :

(cid:1) ∑R1 = R U F U X U {  , (cid:218) (cid:1) ∑R1 = R U F U X U {  , (cid:218)

} U { F, V } U { , } U {(cid:2)} } U { F, V } U { , } U {(cid:2)}

(cid:1) FR1 = { clauses du 1er ordre construites sur ∑

R1R1R1R1 }

(cid:1) AR1 = Ø

(aucun axiome)

ENSI

Logique Mathématique

suite

42

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

(cid:1) R R1 (règles d’inférence) - résolution

C’ (cid:218)

A’ et A’’ des atomes et s

- factorisation

C’’ (cid:218)

 A’’

(cid:218) A’ C’s p.g.u de A’ et A’’ (A’s

(cid:218) C’’ s

Res

l’

l’’

C (cid:218) C s C s p.g.u de l’ et l’’ (l’s

Fact

l’s l’s

= A’’s )

= l’’s

)

l’ et l’’ des littéraux et s (cid:4) Il faut que deux clauses différentes

n’ont pas de variables communes ► renommage

Cas particulier :

A’

(cid:2)

 A’’

Res

si A’s

= A’’s

ENSI

Logique Mathématique

43

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) s s s (cid:218) (cid:218) (cid:218) s s s (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) s s s (cid:218) (cid:218) (cid:218) (cid:218) s s s s s s (cid:218) (cid:218) (cid:218) (cid:218) s s s La méthode de résolution

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

(cid:4) Il faut utiliser le renommage

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

" x P(x) (cid:217) " x P(x) (cid:217)

" x Q(x) " x Q(x)

or "

" x P(x) (cid:217)

" x Q(x) ≡ "

" x P(x) (cid:217)

" y Q(y)

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

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

ENSI

Logique Mathématique

44

" " (cid:217) (cid:217) (cid:217) " " " " " (cid:217) (cid:217) (cid:217) " " " " " (cid:217) (cid:217) (cid:217) " " " " " (cid:217) (cid:217) (cid:217) " " " La méthode de résolution

Exemple (cid:1)

P(x) (cid:218)

(cid:218) Q(x)  P(a) (cid:218)

(cid:218) R(x)

renommage

P(x) (cid:218)

(cid:218) Q(x)  P(a) (cid:218)

(cid:218) R(y)

Q(a) (cid:218)

(cid:218) R(y)

Res

avec s = { x ← a } avec s = { x ← a }

(cid:1)

P(x) (cid:218)

(cid:218) P(f(y)) (cid:218)

 Q(x)

P(f(y)) (cid:218)

 Q(f(y))

Fact

avec s = { x ← f(y)}

ENSI

Logique Mathématique

45

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Proposition

(cid:1) Si

{ C1 , C2 }

Res

C

alors

{ C1 , C2 } ╞ C

autrement dit

{ C’ (cid:218)

l’ , C’’ (cid:218)

 l’’ } ╞ C’s avec s

(cid:218) C’’s

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

(cid:1) Si C1

Fact

C

alors

C1 ╞ C

autrement dit

{ C’ (cid:218)

l’ (cid:218)

l’’ } ╞ C’s avec s

l’s

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

ENSI

Logique Mathématique

46

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Preuve

(cid:218) C’’s

l’ , C’’ (cid:218)

 l’’ }╞ C’s (cid:1) { C’ (cid:218) Soit I une interprétation telle que [C’ (cid:218) , [C’ s alors pour tout s en particulier si l’s = l’’s [ l’’s [ l’’s - si [l’s - si [l’s [C’’s

l’ s , alors ]I = F ] = F ]I = V

]I = V alors ] = V alors donc forcément

]I = [C’’ s

avec s

p.g.u de l’ et

l’’

l’ ]I = [C’’ (cid:218)  l’’ s

]I = V

 l’’ ]I = V

- si [l’s

]I = F alors forcément

[C’s

]I = V et donc [C’s

et donc [C’s

(cid:218) C’’s

]I = V

(cid:218) C’’s

]I = V

(cid:1) { C’ (cid:218)

l’ (cid:218)

l’’ } ╞ C’s

l’s

avec s

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

même principe

ENSI

Logique Mathématique

47

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) 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 c-a-d Soit ℰ un ensemble de clauses

ℰ est insatisfiable ssi

ℰ (cid:2) R1

ENSI

Logique Mathématique

48

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 Ω 2. Renommer les variables des différentes clauses de Ω 3. Tant que ( (cid:2) ∉ Ω )

faire ∈ Ω telles que {Ci , Cj }

C »

Res

- choisir « Ci et Cj

ou « Ci

∈ Ω telle que Ci

C »

Fact

- Ω := Ω U {C}

ENSI

Logique Mathématique

49

La méthode de résolution

Exemple

{ P(x) (cid:218)

(cid:218) P(f(x)) , P(a) ,  P(f(x)) }

Renommage {  P(x) (cid:218)

(cid:218) P(f(x)) , P(a) ,  P(f(y)) }

{x ← a}

P(f(a))

{y ← a}

(cid:2)

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

ENSI

Logique Mathématique

50

(cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Exemple (suite) { P(x) (cid:218)

(cid:218) P(f(x)) , P(a) ,  P(f(y)) }

Autre présentation

 P(x) (cid:218)

(cid:218) P(f(x)) P(a)

{x ← a}

P(f(a))  P(f(y))

(cid:2)

{y ← a}

ENSI

Logique Mathématique

51

(cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Exemple

H1 : «Tout animal à plumes est un oiseau »

(cid:3) "

" x P(x) ⇒⇒⇒⇒ O(x)

H2 : «Aucun mammifère n’est un oiseau » (cid:3) "

" x M(x) ⇒⇒⇒⇒  O(x)

C : «Donc, aucun mammifère n’a de plumes »

(cid:3) " (cid:3) "

" x M(x) ⇒⇒⇒⇒  P(x) " x M(x) ⇒⇒⇒⇒  P(x)

(cid:4) 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) (cid:217)

(cid:217) P(x)}

ENSI

Logique Mathématique

suite

52

" " " " " " " " " " " " $ $ (cid:217) (cid:217) La méthode de résolution

1. Forme clausale

{  P(x) (cid:218)

(cid:218) O(x) ,  M(x) (cid:218)

 O(x) , M(a) , P(a) }

2. Renommage {  P(x) (cid:218)

(cid:218) O(x) ,  M(y) (cid:218)

 O(y) , M(a) , P(a) }

3. Résolution

{  P(x) (cid:218)



(cid:218) O(x) ,  M(y) (cid:218)



 O(y) , M(a) , P(a) } 

{y ← a}

 O(a)

{x ← a}

 P(a)

ENSI

Logique Mathématique

53

(cid:2)

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) 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 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 le (cid:2) s’il 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 le (cid:2) s’il existe

ENSI

Logique Mathématique

54

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 le (cid:2)

ENSI

Logique Mathématique

55

La méthode de résolution

Différentes stratégies possibles (cid:1) 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

(cid:4) la stratégie linéaire est une stratégie complète

(cid:1) 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)

(cid:4) la stratégie linéaire input n’est pas une stratégie complète suite

ENSI

Logique Mathématique

56

Res

La méthode de résolution

C’ C’’ C’ , C’’ ∈ ℰ

D1

B1

......

Dk

Bk

...... ......

• stratégie linéaire Bk

∈∈∈∈ ℰℰℰℰ U {D1 , ... , Dk-1}

• stratégie linéaire input Bk

∈∈∈∈ ℰℰℰℰ

ENSI

Logique Mathématique

57

La méthode de résolution

Exemple

{ p (cid:218)

q ,  p (cid:218)

(cid:218) q , p (cid:218)

 q ,  p (cid:218)

 q }

q (cid:218)

q  q (cid:218)

 q

q  q q  q

(cid:2)

(cid:4) stratégie non linéaire

ENSI

Logique Mathématique

58

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Exemple

{ p (cid:218)

q ,  p (cid:218)

(cid:218) q , p (cid:218)

 q ,  p (cid:218)

 q }

q (cid:218)

q

q

(cid:4) mais non input

(cid:4) stratégie linéaire

 p

 q

(cid:2)

(cid:4) il est facile de vérifier

qu’une stratégie linéaire input ne va pas donner le (cid:2) (boucle)

ENSI

Logique Mathématique

59

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Exemple

{  p , p (cid:218)

q ,  q (cid:218)

r ,  r }

q

r

(cid:2)

(cid:4) stratégie linéaire input

ENSI

Logique Mathématique

60

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) 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

(cid:1) Une stratégie est dite négative (resp. positive) si à chaque , une des deux clauses fois qu’on applique la règle Res , une des deux clauses fois qu’on applique la règle

parentes est une clause négative (resp. positive) c-à-d ne

contenant que des littéraux négatifs (resp. positifs)

(cid:4) les stratégies négatives sont des stratégies complètes.

De même les stratégies positives

ENSI

Logique Mathématique

61

La méthode de résolution

(cid:1) Une stratégie est dite ordonnée si les littéraux de chaque

clause sont ordonnés et la 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 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

(cid:4) une stratégie à la fois linéaire et ordonnée est une

stratégie complète

ENSI

Logique Mathématique

62

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 • 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

ENSI

Logique Mathématique

suite

63

La méthode de résolution

C

Res

B0

D1

B1

......

Dk

Bk ......

∈ ℰ

C, B0 , ... , Bk C négative D1 , ... , Dk négatives

(cid:4) chaque clause résolvante Di est forcément une clause l- 1

négative de la forme  A (cid:218)

(A un atome)

... (cid:218)

l- n

(cid:4) à chaque itération i , on choisit une clause Bi l’m telle que il existe s

forme A’ (cid:218) A et A’ et on applique la règle Res (on dit on coupe sur les premiers littéraux de tête)

∈∈∈∈ ℰ de la p.g.u de

... (cid:218)

l’1

ENSI

Logique Mathématique

64

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Remarques (cid:1) 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

(cid:1) Une clause de Horn est une clause contenant au plus un

littéral positif

(cid:1) On doit au moins avoir une clause initiale complètement (cid:1) On doit au moins avoir une clause initiale complètement

négative pour pouvoir initialiser la SLD Resolution

(cid:1) En adoptant la stratégie SLD, la règle de factorisation (Fact)

n’est plus nécessaire

(cid:1) Une stratégie SLD peut nous aider à savoir si un ensemble de

clauses est éventuellement satisfiable (mais pas systématiquement)

ENSI

Logique Mathématique

65

La méthode de résolution

Mise en œuvre de la SLD Resolution • l’ensemble des clauses initiales est ordonné comme suit : n , C1+

1 , ... , C1+

ℰ = { C-

1 , ... , C-

1 , ... , l+

m , l+

p }

C-

i : clauses négatives j : clauses de Horn avec un seul littéral positif

C1+

le littéral positif est placé en tête 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 Mathématique

66

La méthode de résolution

Exemple SLD resolution

{  p (cid:218)

 q , q (cid:218)

 r , p (cid:218)

 s , r

, s }

 q (cid:218)

 s

 r (cid:218)  r (cid:218)

 s  s

 s

(cid:2)

ENSI

Logique Mathématique

67

(cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) (cid:218) La méthode de résolution

Exemple

{  p (cid:218)

 q , q (cid:218)

 r , p (cid:218)

 s , r , s }

 p (cid:218)

 r

 p 

(cid:4) n’est pas une stratégie SLD

car ord