Logique des Prédicats : Fondements, Syntaxe et Sémantique

aire dans D (un

sous-ensemble de Dk

Interpr tation des termes

On d nit une fonction dinterpr tation I par

Terme

constante c

variable x

f (t1, . . . , tn)

I(Terme)

I(c)

I(x)

I(f )(I(t1), . . . , I(tn))

Exemple 5.2. On a une interpr tation I d nie par

un domaine D =

0, 1, 2, 3

}

{

Universit de Gen ve G. Falquet

c

48

5.3. S MANTIQUE

I(a) = 0, I(b) = 1, I(c) = 2, I(d) = 3

I(f ) =

0, (1, 0)

(0, 0)

{

I(x) = 1, I(y) = 0

0, (0, 1)

2, (2, 3)

2, (3, 3)

3,

3 pour le reste

}

calcul de quelques interpr tations de termes selon I :

I(a) = 0

I(f (a, x)) = I(f )(0, 1) = 0

I(f (x, f (y, b))) = I(f )(1, I(f )(0, 1)) = I(f )(1, 0) = 2

Interpr tation des atomes

Le principe dinterpr tation des atomes consiste valuer les termes donn s comme

param tres au pr dicat puis voir si le n-uplet de termes obtenu fait partie de linterpr -

tation du pr dicat.

I(p(t1, . . . , tn) = v

si et seulement si

(I(t1), . . . , I(tn))

I(p)

La relation qui forme linterpr tation I(p) du pr dicat p fournit donc lensemble des

valeurs de param tres pour lesquels on veut que le pr dicat soit vrai.

Linterpr tation des atomes tant d nie, on peut interpr ter toutes les formules pos-

en utilisant les m mes r gles quen logique des

s dant des connecteurs logiques

propositions.

'(

Extension aux formules avec quanticateurs

Pour interpr ter les formules quanti es on commence par introduire la notion de

variante dune interpr tation. On dit quune interpr tation J est une variante de I en x

si J est partout identique I, sauf pour la variable x.

On note Ix=d la variante de I o I(x) = d (d

D)

Remarque. I est une variante de I en x (qui consiste reprendre la m me valeur pour

x)

On peut alors interpr ter les formules quanti es en appliquant les deux r gles sui-

vantes :

1. Quantication universelle

si et seulement si pour tout d

D on a

I(

x ) = v

Ix=d( ) = v

Universit de Gen ve G. Falquet

c

49

5.3. S MANTIQUE

autrement dit, la formule doit tre vraie pour toutes les valeurs possibles de la variable

x quanti e.

2. Quantication existentielle

I(

x ) = v

si et seulement si il existe un l ment d

D tel que

Ix=d( ) = v

Exemple 5.3. Soit le vocabulaire compos des symboles :

constantes a, b, c, d, k1, k2, k3, k4

pr dicats P (unaire), E (unaire), C (unaire), I (binaire)

variables x, y, z, u, v, w

On interpr te ce langage dans le domaine compos des tudiants, des cours, des personnes

et des inscriptions dune (micro) universit . Le domaine est lensemble D = Personne

Etudiant

Cours, o

*

*

Personne =

Etudiant =

Cours =

Alice, Bob, Charles, Diane

{

Alice, Bob, Charles

{

C1122, C1101, M2001, M2002

{

}

}

}

Linterpr tation des constantes est donn e par :

I(a) = Alice, I(b) = Bob, I(c) = Charles, I(d) = DianeI(k1) = C1122, I(k2) =

C1101, I(k3) = M2001, I(k4) = M2002

et linterpr tation des pr dicats par

I(P ) = Personne, I(E) = Etudiant, I(C) = Cours

I(I) = Inscription =

(Alice, Histoire), (Bob, Chimie), (Charles, Histoire)

}

.

{

(La gure 5.1 r sume graphiquement cette interpr tation.)

Interpr tons quelques formules selon I

1. I(a) = Alice

2. I(C(k3)) = v car I(k3) = M2001 et M2001

3. I(C(a)) = f car Alice

4. I(I(c, k1)) = v car (Charles, C1122)

5. I(

6. I(

7. I(

y I(x, y)) = f car Ix=M2001(

y I(x, y))) = vrai car

x I(x, C1101)) = v car Ix=Bob(I(x, C1101)) = v.

x

I(C).

I(C)

I(I)

x(E(x)

Ix=Alice(E(x)

y I(x, y)) = v (prendre y = C1122)

y I(x, y)) = f (entre autres).

Universit de Gen ve G. Falquet

c

50

5.3. S MANTIQUE

a

b

c

d

k1

k2

k3

k4

P

E

Bob

Alice

Charles Diane

Etudiant

Personne

C1101

M2002

C1122

M2001

Cours

Inscription

I

C

Figure 5.1 Une interpr tation du vocabulaire a, b, c, d, k1, k2, k3, k4, P, E, I, C

y I(x, y)) = v (prendre y = C1101)

Ix=Bob(E(x)

Ix=Charles(E(x)

y I(x, y)) = v (prendre y = C1122)

et E(x) = f , donc la formule est vraie, pour toutes les autres valeurs de x.

Lorsquon value une formule il faut faire attention aux fait que deux variables qui portent

des noms di rents peuvent repr senter la m me valeur du domaine.

Exemple 5.4. Si on consid re linterpr tation J d nie par

D =

J(ville) =

J(distance) =

Milan, Tokyo, Oslo

{

N

Milan, Tokyo, Oslo

}

{

}*

La formule

(Milan, Tokyo, 9710), (Milan, Oslo, 1608), (Oslo, Tokyo, 8401)

}

{

x

y(ville(x)

ville(y)

'

z (distance(x, y, z)

distance(y, x, z))

(

repr sente le fait quentre deux villes il y a toujours une distance (z). Cependant elle

est fausse dans linterpr tation J car les variables x et y peuvent repr senter la m me

ville. Pour rendre la formule vraie il faudrait ajouter linterpr tation de distance :

(Milan, Milan, 0), (Tokyo, Tokyo, 0), (Oslo, Oslo, 0).

Propri t s des formules ferm es

Les formules ferm es repr sentant des propositions, on peut reprendre telles quelles

les d nitions de satisabilit , mod le, quivalence et cons quence logique de la logique

des propositions.

D nition 5.3. tant donn une interpr tation I est une formule ferm e f , on note

= A le fait que I(A) = f . Une formule ferm e f et

I

|

= A le fait que I(A) = v et I

|

Universit de Gen ve G. Falquet

c

51

5.4. D DUCTION

satisable sil existe une interpr tation I telle que I

= A, on dit alors que I est un mod le

|

de A. Dans le cas contraire on dit que A est inconsistante. Une formule A est valide si

= A.

I

|

= A pour toute interpr tation , on note

|

Exemple 5.5. Lensemble de formule

F =

{

p(a, b),

y p(a, y)

}

est inconsistant car pour avoir I(p(a, b)) = v il faut n cessairement que (I(a), I(b))

y p(a, y)) = f . Les deux formules ne peuvent jamais tre vraies

I(p). Mais alors I(

simultan ment. La formule

(

est valide. Si linterpr tation I(P ) contient tous les l ments du domaine D la partie

gauche de la formule est vraie, si ce nest pas le cas, cest la partie droite qui est vraie.

x P (x))

(

y

(

P (y))

5.4 D duction

Les r gles de d duction naturelle pour la logique des propositions restent valables.

Pour obtenir un syst me complet il faut leur adjoindre des r gles sp cique aux formules

quanti es :

Elimination du quanticateur universel

SI F (x) est une formule o x est libre et t est un terme qui ne contient aucune variable

li e de F , on peut remplacer x dans

x F (x) par t pour obtenir F (t)

x F (x)

1.

2. F (t)

Exemple :

de

x(x + 1 > x) on peut d duire 3 + 1 > 3.

Introduction de

Si on a pu d duire une formule F (x) o x est libre alors on peut d duire

1. F (x)

2.

En g n ral la variable x est introduite dans une hypoth se.

x F (x)

x F (x)

Universit de Gen ve G. Falquet

c

52

5.5. NORMALISATION ET R SOLUTION

Introduction de

Si on a d duit une formule F (t) qui contient un terme t (p.ex. une constante) on peut

en d duire quil existe un x qui satisfait F (x)

x F (x)

1. F (t)

2.

Exemple

1. 0.52 < 0.5

x(x2 < x)

2.

Suppression de

partir de

x F (x) on peut formuler une hypoth se F (y) puis faire des d ductions

avec elle.

1.

2.

3.

4. R ( limination de il existe dans 1 et 3)

x F (x) (hypoth se)

F (y) (y variable nouvelle)

R (d duction partir de 2)

Exemple de d duction

x A(x)]

[

A

y

[

A(y)] hypoth se

A(t)]

[

A(t)

y

(

x A(x)

limination

A(y))

y

(

Ҭ

A(y))

absurde

importation et introduction de

5.5 Normalisation et R solution

Lapplication de r gles dinf rence telles que le principe de r solution exige la mise en

forme normale des formules. Dans le cas de la logique des pr dicats cette mise en forme

se fait en quatre tapes :

1. Mise en forme prenex (d placement de tous les quanticateurs au d but de la for-

mule)

2. Skolemisation (suppression des

)

Universit de Gen ve G. Falquet

c

53

5.5. NORMALISATION ET R SOLUTION

3. Mise en forme normale conjonctive

4. Mise en forme clausale (suppression des

)

Forme prenex

Une formule est dite en forme prenex si tous ses quanticateurs apparaissent au d but.

Il est toujours possible de transformer une formule en une formule quivalente sous forme

prenex. Pour cela on applique autant de fois que n cessaire les quivalences

x w

x

a

w

x w

x

a

w

x w1)

(

w2 a

x(w1 '

'

w2) si x napparait pas dans w2

x w1)

(

w2 a

x(w1 (

(

w2) si x napparait pas dans w2

Exemple 5.6. La mise en forme prenex pr serve les quanticateurs

z A(x, z))

x

y(E(x, y)

x

y(

a

y

x

a

y

x

a

E(x, y)

z(

z(E(x, y)

E(x, y)

(

(

z A(x, z))

A(x, z))

A(x, z))

Exemple 5.7. La mise en forme prenex modie les quanticateurs

x((

y(A(x, y))

a

a

a

a

y(A(x, y))

A(x, y))

A(x, y)

x(

(

x((

y

y(

x(

y(A(x, y)

x

B(x))

B(x))

B(x))

B(x)))

(

(

(

B(x))

Skolemisation

Le but de cette op ration est de supprimer les quanticateurs

sation provient de lobservation suivante : lorsque on a une formule du type

. Lid e de la skol mi-

x

y p(x, y)

(5.1)

54

Universit de Gen ve G. Falquet

c

5.5. NORMALISATION ET R SOLUTION

cela signie que pour chaque x on peut trouver au moins un y tel que p(x, y). Donc

on peut d nir une fonction f (x) qui nous fournit une valeur y = f (x) telle que p(x, y)

est vraie. Ceci qui nous permet de r crire la formule 5.1 comme

Sil y a plusieurs quanticateurs universels, la fonction d pend de toutes les variables

x p(x, f (x))

qui viennent avant y dans la formule.

Exemple 5.8. Skolemisation

1. A1 =

x

y

z(E(x, y)

A(x, z)).

sk(A1) =

x

y(E(x, y)

A(x, f (x, y))).

2. A2 =

x

u

y

z(P (x, u)

(Q(u, y)

R(y, z))).

sk(A2) =

x

'

y(P (x, f (x))

(Q(f (x), y)

'

R(y, g(x, y)))).

La skolemisation ne conserve pas le sens des formules. En g n ral sk(A) nest pas quiva-

lente A, mais

Th or me 5.1. A est satisable si et seulement si sk(A) lest.

Par cons quent, pour d montrer que

on peut d montrer (par exemple avec le principe de r solution) que

f1, . . . , fn} |

= g

{

sk(f1), . . . , sk(fn), sk(

g)

}

{

est inconsistant.

Forme clausale

Un fois que la formule a t skol mis e il ne reste que des variables quanti es univer-

sellement. On peut donc se passer de l criture explicite des quanticateurs. La formule

restante est compos e datomes et de connecteurs logiques. On peut alors appliquer la

m me technique quen logique propositionnelle pour la mettre en forme normale conjonc-

tive, puis sous forme dun ensemble de clauses.

Universit de Gen ve G. Falquet

c

55

5.5. NORMALISATION ET R SOLUTION

Exemple 5.9. Si on repart de la formule skol mis e

sk(A2) =

x

y(P (x, f (x))

(Q(f (x), y)

'

R(y, g(x, y))))

, l limination des quanticateurs universels donne

P (x, f (x))

(Q(f (x), y)

'

R(y, g(x, y)))

. En appliquant la transformation

on obtient

(

P (x, f (x))

(

(Q(f (x), y)

'

R(y, g(x, y)))

. Puis par distributivit

P (x, f (x))

(

(

Q(f (x), y))

P (x, f (x))

(

'

(

R(y, g(x, y)))

et donc deux clauses :

1.

2.

P (x, f (x))

P (x, f (x))

Q(f (x), y))

R(y, g(x, y))

(

(

Application du principe de r solution en logique des pr dicats

On se rappel que la r gle de r solution en logique propositionnelle stipule qu tant

donn deux clauses

et

C1 = L1 (

. . .

Li (

(

. . .

(

Lm

C2 = M1 (

. . .

Mj (

(

. . .

(

Mn

o Li = p et Mj =

Le r solvant de C1 et C2 sur Li et Mj est la clause

p.

Li

. . .

CR = L1 (

Lm (

Dans le cas de la logique des pr dicats, on peut eectuer la r solution sur deux litt raux

P (u1, . . . , un) non seulement sils sont gaux mais galement si les ti et

Mj+1 (

Li+1 (

M1 (

1 (

1 (

Mn

Mj

. . .

. . .

. . .

(

(

(

(

P (t1, . . . , tn) et

ui uniables.

D nition 5.4. Deux formules atomiques sont uniables sil existe une substitution des

variables par des termes qui rend les deux formules identique.

Universit de Gen ve G. Falquet

c

56

5.5. NORMALISATION ET R SOLUTION

Par exemple, les formules atomiques P (x, a, y) et P (c, a, z) , o a et c sont des

constantes, sont uniables par la substitution x

c, y

z .

Par contre P (x, a, y) et P (c, b, z) ne sont pas uniables car les constantes a et b ne

peuvent tre uni es (on ne peut remplacer une constante par une autre).

Exemple 5.10. R solution avec unication

C1 =

P (x)

(

Q(y)

(

R(x, y)

C2 = Q(a)

C3 = P (b)

y

x

a sur C1 permet la r solution avec C2 :

CR =

b sur CR, r solution avec C3 :

P (x)

(

R(x, a)

CS = R(b, a)

Comme en logique des propositions, on emploie g n ralement la r solution pour faire

des preuves par r futation.

Exemple 5.11. On veut montrer que les trois formules

x ((S(x)

f1 =

P (x)) , f2 =

T (x))

ont pour cons quence la formule P (a) .

Passage en forme clausale :

(

x (S(x)

(

R(x)) , f3 =

R(a)

et produit donc les deux clauses

f1 a

x (S(x)

(

P (x))

'

x (T (x)

(

P (x))

C1 =

S(x)

C2 =

T (x)

P (x)

P (x)

(

(

f2 a

C3 = S(x)

R(x)

(

f3 a

C4 =

R(a)

.

La n gation de la cons quence cherch e donne

C5 =

P (a)

Universit de Gen ve G. Falquet

c

57

5.5. NORMALISATION ET R SOLUTION

Par r solution sur R de C3 et C4 avec x

a on produit

Par r solution sur S de C1 et C6 on produit

C6 = S(a)

C7 = P (a)

Enn C5 et C7 donnent la clause vide. On a donc prouv la cons quence logique.

Universit de Gen ve G. Falquet

c

58