III Sémantique de la logique des Prédicats

Pour donner un sens à une formule de la logique des prédicats il faut indiquer :
 Quels sont en réalité les objets (constantes, variables, termes) dont parle la formule
 A quoi renvoient en réalité les symboles de prédicats et de fonctions qui apparaissent
dans la formule
 Interpréter les symboles non logique du langage

3.1-Interprétation des formules ( équivalent d’une valuation en CP0)

Une interprétation d’une formule F consiste en un ensemble non vide D et une affectation
d’une valeur à chaque constante, symbole de fonction et symbole de relation qui apparaissent
dans F comme suit :
On affecte un élément de D à chaque constante
On affecte une fonction de Dn I  D à Chaque symbole de fonction n-aire (d’arité n)
(f)

On affecte une Relation de D 

n
0,1à Chaque symbole de Relation d’arité n.
I ( P)

Exemples

Définition
Pour toute interprétation d’une formule  dans un domaine D,  est évaluée à vrai ou faux
selon les règles suivantes
 Si on connaît la valeur de vérité de 1 et  2 alors la valeur de vérité de 1 , 1  2 ,
1  2 , 1  2 , 1   2 est obtenue conformément aux règles du chapitre précédent.
 x(1 ) est évaluée à vrai ssi 1 est évaluée à vrai pour tout élément du domaine D,
sinon elle est évaluée à faux.
 x(1 ) est évaluée à vrai ssi 1 est évaluée à vrai pour au moins un élément du
domaine D, sinon elle est évaluée à faux

Remarques
 Toute formule contenant des variables libres (ne sont pas quantifiées), ne peut être
évaluée
 On suppose dans la suite que les formules considérées ne contiennent pas de variables
libres ou si elles contiennent des variables libres, celles-ci doivent être traitées comme
des variables quantifiées universellement x

Exemples

7
Définition
 Une formule F est satisfaisable ssi  une interprétation I tel que : F est évaluée à vrai
dans I. I est dit modèle de F et I satisfait F
 Une formule F est insatisfaisable ssi il n’existe aucune interprétation satisfaisant F
F est insatisfaisable
 Une formule F est valide ssi chaque interprétation I est un modèle de F.
Exemples

3.2 Conséquences logiques

Définition Une formule F est une conséquence logique des formules F1 , F2 .....Fn ssi pour
chaque interprétation I, si F1  F2 ...  Fn est vrai dans I alors F est aussi vrai dans I
Exemples

Remarque
Dans le calcul des prédicats, il y a en général, une infinité de domaines et un nombre infini
d’interprétations, on ne peut donc pas vérifier la validité ou l’inconsistance d’une formule
en l’évaluant de toutes ses interprétations possibles. On a besoins d’une méthode de
preuve syntaxique

8
3.3- Problème de validité

Le problème de validité revient à trouver un algorithme qui décide si une formule donnée est
valide ou non.
 Ce problème de validité admet une solution dans la CP0
 Ce problème de validité admet une solution partielle dans la CP1
La notion de solvabilité partielle est équivalent à l’existence d’un algorithme qui prend en
entrée une formule ( sous une forme normale que l’on définira ultérieurement et
 Répond Oui si la formule est valide
 Répond Non ou continue à boucler indéfiniment si la formule n’est pas valide

IV-Manipulations algébriques
4.1-Equivalence et notations
On définit la relation  comme dans le CP0 par
   ssi  
Cette relation est une relation d’équivalence, il ya dualité des quantificateurs par rapport à la
négation ( est ) et ( est )

4.2- Forme normale prénexe

Pour simplifier les procédures de preuves qu’on va étudier, on a besoin de transformer les
formules de CP1 en formules dites en forme normale prénexe (f.n.p.)
Définition
Une formule  du CP1 est dite en forme normale prénexe si elle est de la forme :

Q1 x1 Q2 x 2 .....Qn xn 

M
préfixe matrice

Où Qi est un quantificateur
M une formule sans quantificateur

Exemples
1  x y Px, y   Q y  en f.n.p.
2  xy Px, y   Q y  en f.n.p
3  xPx  zQz  n’est pas en f.n.p
4  xyQ y, y   Px  n’est pas en f.n.p

4.3 Equivalences sémantiques

*  une formule avec x variable libre dans  , on note [x]
*  formule ne contenant pas la variable x

9
* Q un quantificateur quelconque
On a les équivalences sémantiques suivantes :

(1a) Qx  [ x]    Qx [ x]   

(1b) Qx  [ x]    Qx [ x]   
(2a) (x) [ x]  x [ x]
(2b) (x) [ x]  x [ x]

Considérons maintenant [x] et  [x]

(3a) x[ x]  x [ x]  (x)[ x]   [ x]
(3b) x[ x]  x [ x]  (x)[ x]   [ x]

Attention
(3a) x[ x]  x [ x]  (x)[ x]   [ x]
(3b) x[ x]  x [ x]  (x)[ x]   [ x]

Exemple

Remarque
Il faut faire attention en manipulant de telles formules
xP( x, y )  xP( x)  (x)(y )P( x, y )  P( x) 

Attention : Pour pouvoir transformer x[ x]  x [ x] il faut utiliser une nouvelle variable z
x[ x]  x [ x]  x[ x]  z [ z ]
 xz [ x]   [ z ]
(z n’apparaît pas dans  )
x[ x]  x [ x]  x[ x]  z [ z ]
 xz [ x]  [ z ]

Ainsi pour ces deux cas, on peut toujours rassembler les quantificateurs en tête de la formule,
et l’on aura en général
(4a) Q1 x  [ x]  Q2 x  [ x]  Q1 x Q2 z [ x]   [ z ]
(4b) Q1 x  [ x]  Q2 x  [ x]  Q1 x Q2 z [ x]   [ z ]
Q1 et Q2  ,  et z  var [ x]

Proposition

Toute formule est équivalente à une formule en f.n.p. ( Mise en facteur des quantificateurs)

10
Démo :
La démonstration de ce théorème est constructive  elle permet d’exhiber une forme prénexe
équivalente à une formule close donnée

Algorithme :

Etape1 : Eliminer les connecteurs et  en utilisant les équivalences sémantiques

suivantes :
     (  )  (   )
      
Etape2 : Ramener les signes de négation immédiatement devant les atomes avec les lois :
    
        
        
 (2a) (x) [ x]  x [ x]
 (2b) (x) [ x]  x [ x]
Etape3 : Renommer les variables si nécessaire.
Etape4 : Ramener les quantificateurs au début de la formule pour obtenir la f.n.p. en utilisant
(1a), (1b), (3a), (3b), (4a),(4b).
Exemples :

Remarque : Attention ! l’ordre des quantificateurs de nature différentes est important.

Considérer l’exemple suivant :
x y x  y et y x x  y
 
vrai dans IN faux
( toute élément x de IN peut être majoré) car il n ' ya pas de plus petit
element dans IN

V Mise sous forme standard de Skolem

Considérons une formule close prénexe; son préfixe est en principe constitué, s'il existe,
d'une alternance quelconque de quantifications universelles ou existentielles.

Nous allons montrer comment on peut lui associer une formule close prénexe de même
sens dont le préfixe est soit absent, soit constitué de quantifications universelles.

11
Soit par exemple la formule xA qui s'énonce: "il existe au moins un objet x tel que A".
Si l'on choisit de symboliser l'un de ces objets par un nouveau symbole de constante c
on peut penser que la formule Ac x  , où toutes les occurences de la variable x sont
remplacées par c a le même sens que la formule initiale.

Soit maintenant la formule xyA qui se lit "pour tout objet x il existe au moins un objet
y tel que A" ou plus précisément" à chaque objet x correspond au moins un objet y tel
queA". Si l'on choisit parmi les objets y qui conviennent, l'un d'entre eux on établit une
relation fonctionnelle entre x et y que l'on peut représenter par un nouveau symbole de
fonction f1, et on est en droit de penser que la formule " xA f x y , où toutes les
occurrences de y sont remplacées par le terme f  x  a un rapport sémantique étroit avec
la formule de départ ;

Étant donnée une formule close prénexe, on appelle forme de Skolem de F ou plus
simplement skolémisée de F( ou bien la forme standard de Skolem (f.s.s.)) , la formule Fs
obtenue en éliminant toutes les quantifications existentielles du préfixe de F en
remplaçant, dans la formule qui suit le préfixe, chaque variable gouvernée par un
quantificateur existentiel :

 Par un symbole de constante inédit si le quantificateur existentiel n'est pas

précédé par des quantificateurs universels.
 Par un terme t=fn (x1, x2,...,xn) où fn désigne un symbole inédit de fonction à n
variables, si la quantification existentielle est dans la portée de n
quantificateurs universels portant respectivement sur les variables x1, x2,...,xn.

Exemples :

1/Considérons, le langage LI = {P1,Q2,f1,g3,a,b} et la formule close prénexe

F  xyzt Qx, y   Pg a, z, t 

Si l'on note c un nouveau symbole de constante et h2 un nouveau symbole de fonction à deux

variables, la skolémisée de F s'écrit

Fs  yzQc, y   Pg a, z, h y, z 

Puisque dans un premier temps on a formé

yzt Qc, y   Pg a, z, t 

à l'aide de la substitution [c | x]et qu'on a formé ensuite Fs à l'aide de la substitution h y , z  t  .

Les constantes et les fonctions utilisées pour remplacer les variables existantes sont appelées
fonctions de Skolem

Remarquons que dans l’exemple1 la formule Fs est une formule du nouveau langage

12
 L1'  {Pl, Q2, f1, g3, h2, a, b, c}

Il ne saurait être question d'affirmer que F et Fs sont des formules équivalentes

puisqu'elles ne sont pas construites sur le même langage.

2/Considérons les formules closes prénexes, cherchons à déterminer leurs skolémisées

  xyzuvwPx, y, z , u, v, w

  xyzwuvRx, y   F z , u, v   K w  G v 

  xyz Px, y   Qx, z   Rx, y, z 

 Un ensemble S de clauses considéré comme la conjonction de toutes les clauses,

où les variables sont supposées quantifiées universellement
 La forme standard de Skolem (f.s.s.) peut être représentée par un ensemble de
clauses

 La Skolémisation ne préserve que la satisfaisabilité et non pas

l’équivalence  Elle ne préserve que l’insatisfaisabilité, elle convient aux
techniques réfutationnelles

Théorème (existence d’une forme de Skolem)

Etant n’importe quelle formule F en forme prénexe, il existe une formule Fs dite skolémisée
de F telque

 Si F contient n quantificateurs existentiels, n nouveau symboles de fonctions

apparaissent dans F (fonctions de skolem)
 Fs ne contient pas de quantificateurs existentiels
 F est satisfaisable ssi Fs est satisfaisable

Remarques : 1/On a toujours Fs  F mais pas toujours F  Fs

2/Dans le cas général, on n’a pas équivalence sémantique c’est à dire F  Fs

exemples

13
3/Quand F insatisfaisable alors F  Fs

4/Une formule F peut avoir plusieurs formes de Skolem. On adopte donc l’approche suivante
F  F1  F2 ....  Fn
n
Fs   ( Fi ) s
i 1

Remarque:

Le but de cette méthode est de dégager une méthode permettant de transformer un ensemble E
de formules du calcul des prédicats en un ensemble de clauses CE  forme normale
conjonctive d’une formule A sans quantificateurs  On entend la même chose que dans le cas
propositionnel, la seule différence est dans la syntaxe des littéraux

VI Méthode de résolution
Rappelons que les deux règles qui forment l'ossature de la méthode de résolution, la
règle de coupure et la règle de simplification, s'appliquent à des formules particulières:
les clauses.

Alors qu'en logique des propositions celles-ci étaient du type

p1  p2  ...  pn  q1  q2  ...  qm

où les pi et qj sont des variables propositionnelles, les clauses de la logique des prédicats
s'écrivent

P1  P2  ...  Pn  Q1  Q2  ...  Qm

où les symboles Pi et Qj désignent en réalité les formules atomiques

Pi (tl, ... , tk) et Qj (t1, ... , tl)

On conçoit donc qu'il faudra prendre en compte la présence de symboles de fonctions,

de symboles de constantes et de variables dans les littéraux d'une clause, pour
appliquer nos deux règles. La difficulté réside dans la fait qu'il faut apparier des

14
littéraux construits à l'aide termes a priori différents,  P (tl,..., tk) et P (t’l,.., t’k) pour la
règle de coupure, et Q (tl, ... , tm) et Q (t'1 ... , t'm) pour la règle de simplification.

La solution consiste à identifier les formules atomiques P (tl,..., tk) et P(t’l,.., t’k) donc les
termes tj et t’j, en procédant à des substitutions à l'intérieur de ces termes. Cette
opération appelée unification repose sur les trois principes suivants:

 Un symbole de constante peut remplacer une variable et non l'inverse.

 Un terme peut remplacer une variable à condition qu'aucune occurrence de cette
variable ne figure dans le terme en question.
 Deux symboles de constantes ou deux symboles de fonctions différents ne
peuvent pas être remplacés l'un par l'autre.

Exemple Considérons le langage L.

 Les formules atomiques Q(a,g(x,y,b)) et Q(x,g(a,b,y)) peuvent être identifiées toutes deux
à la formule Q(a,g(a,b,b)) qui est dite leur unificateur principal en procédant aux
substitutions [a|x] et [b|y]

• On peut unifier Q (x,y) et Q (a,f(x)) en procédant aux substitutions [a|x] et [f(a)| y]

l’unificateur principal est ici Q (a,f(x))

 il est impossible d'unifier Q (f (x) , y) et Q (g (x, a, z) , b) car les symboles de fonction f et

g sont différents.
 il est impossible d'unifier Q (a, x) et Q (b, g(a, b,y)) car les symboles de constantes a et b
sont différents.
 il est impossible d'unifier P(x) et P(g (a, b, x)), le remplacement de x par g(a, b, x) n'est
pas licite, puisque g(a, b, x) contient x. On assisterait sinon à un phénomène de descente
infinie : g(a, b, g (a, b, g (a, b,… )))

Une réfutation (obtention de la clause vide) par coupures et simplifications devra donc
obligatoirement mentionner 1es substitutions qui permettent de la mener à bien. C'est
pourquoi, au lieu de noter de manière habituelle les différentes instances des
applications de nos deux règles, nous les ferons figurer dans un tableau.

Exemple : Considérons les clauses suivantes construites sur le langage

L = {R2,S2, T2, U2,f1,a}

C1=  S (x, x)  U (x, f (x))

C2 =  T(z, f (y))   U (z, f (y))

C3 = R(v, w)  S (v, w)

C4=T(a,u)

C5 =  R (s, t)

15
où x, y, z, u, v, w, s et t désignent des variables et a le symbole de constante présent dans le
langage.

Le tableau suivant indique comment on réfute l'ensemble

Clauses prémisses Règle Nouvelles clauses Clause obtenue Substitutions

C2, C4 Coupure C6 =  U (a, f (y)) [a 1 z],[f(y)1 u]

C3, C5 Coupure C7 = S (v,w) [v 1 s], [w 1 t]

C1, C6 Coupure C8 =  S (a, a) [a 1 x] , [a 1 y]

C7, C8 Coupure  [a 1 v], [a 1 w]

Lorsqu'il s'agit, à l'aide de la méthode de résolution,

 de montrer qu'une formule F est universellement valide, c'est-à-dire que  F,

 de montrer qu'un ensemble de formules {F1,... , Fn} a pour conséquence
sémantique une formule F,

c'est-à-dire que {F1,... , Fn}  F

on sait qu'il faut faire appel à une mise sous forme clausale de la formule  F dans le
premier cas et de la formule F1  F2  ...  Fn  F dans le second cas.

L'obtention d'une telle forme est moins immédiate en logique des prédicats à cause de la
présence des quantificateurs dans la formule, les clauses dont la donnée est chargée de
la représenter ne devant pas contenir de quantificateurs.

Nous procéderons en fait comme suit:

1. Détermination d'une forme prénexe, de la formule qu'il s'agit de réfuter.

2. Détermination de la forme de Skolem associée à cette forme prénexe.
3. Mise sous forme normale conjonctive de la formule qui suit le préfixe de la
formule obtenue à l'étape précédente.
4. Distribution des quantificateurs universels à l'aide de l'équivalence

x A  B   xA  xB

sur chacune des disjonctions (clauses) qui constituent la forme normale

conjonctive en question.

5. Omission des quantificateurs universels et renommage des variables de manière à

faire figurer dans deux clauses distinctes des variables distinctes.

C'est seulement à partir des clauses obtenues à l'étape 5 qu'on mettra en œuvre la

16
méthode de résolution.

Exemple : Soit F  xyzQ  y, z   zQ x, z 

Construites sur le langage L1={Pl, Q2, f1, g3,a, b} . Montrons, à l'aide de la méthode de
résolution que  F .

17