EXERCICE

∀x A(x) |-- ∀ y A(y) ?

F1 : ∀x A(x) hypothèse
F2 : ∀x A(x) → A(y) (SA4)
F3 : A(y) m.p. f1 et f2
F4 : ∀ y A(y) g.

1
 SA1 : (A → (B → A))
SA2 : ((A→ (B → C)) → ((A → B) → (A → C)))
SA3 : ((⎤A → ⎤B) → (B → A))
EXERCICE
SA4 : (∀x A(x) → A(t))
SA5 : ((D → B) → (D → ∀x B))

∀x A(x) |-- ∃y A(y) ?

F1 : ∀y ⎤ A(y) → ⎤ A(t) (SA4)
F2 : ((∀y ⎤A(y) → ⎤A(t)) → (A(t) → ⎤ (∀y ⎤A(y) ))) (SA3)
F3 : (A(t) → ∃ y A(y) ) m.p. f1 et f2
F4 : ∀x A(x) → A(t) (SA4)
F5 : ∀x A(x) hypothèse
F6 : A(t) m.p. f4et f5
F7 : ∃y A(y) m.p.f6 et f3
2
 CALCUL DES PREDICATS DU 1er ORDRE

PROPOSITIONS
Proposition 1 :
Pour tout A : (A→A) est un théorème

Proposition2
Si A1, ... , An-1 |---- (An→B) alors A1, …… , An |--- B

Proposition3 (théorème de déduction) :

Soient A1, ……. , An-1, An des formules closes
Si A1, … , An-1, An |---- B alors A1, …… , An-1 |--- (An→B)

3
 SA1 : (A → (B → A))
SA2 : ((A→ (B → C)) → ((A → B) → (A → C)))
SA3 : ((⎤A → ⎤B) → (B → A))
SA4 : (∀x A(x) → A(t))
SA5 : ((D → B) → (D → ∀x B))

|-- (A→A) ?

F1 : A→(A→A) (SA1)
F2 : (A→ ((A→A)→A)) (SA1)
F3 : (A→ ((A→A)→A)) →((A→(A → A))→(A→A)) (SA2)
F4 : ((A→(A → A))→(A→A)) m.p. F2 et F3
F5 : (A→A) m.p. F1 et F4

4
On a : A1, …………….., An-1|— (An→B)

A-t-on A1, …..…. , An-1, An|— B ?

F1 :
SAi et m.p et les hypothèses

Fp : (An→B)
Fp+1 : An hypothèse
Fp+2 : B par m.p. sur Fp+1 et Fp

5
 Soient A1, ……. , An-1, An des formules closes
Si A1, … , An-1, An |---- B alors A1, …… , An-1 |--- (An→B)
Démonstration du théorème de déduction

Par récurrence sur la longueur K de la déduction

Pour K=1
1er cas : B axiome
F1 : B
F2 : (B->(An->B)) (SA1)
F3 : (An->B) (m.p. F1 et F2)

2ème cas : B est l’une des hypothèses A1, ….. , An-1

F1 : B
F2 : (B->(An->B)) (SA1)
F3 : (An->B) (m .p. F1 et F2)

3ème cas : B est An

|-- (An->B) d’après la proposition 1 et donc A1, …… , An-1 |-- (An->B)

6
 Soient A1, ……. , An-1, An des formules closes
Si A1, … , An-1, An |---- B alors A1, …… , An-1 |--- (An→B)
Démonstration du théorème de déduction

On suppose la propriété vraie pour k<k0

Il ya 4 cas possibles :
(a)B axiome
(b) B = A1ou ….ou An-1 SA2 : ((A→ (B → C)) → ((A → B)→(A → C)))
( c ) B = An
(d) B est obtenu par le m.p. à partir de (C->B) et C
Les cas (a), (b) et (c ) pareil que k=1
(C->B) et C sont des formules de la déduction B à partir des hypothèses (Ai)1≤i≤n
Donc :
A1, ….. , An|-- (C->B) (en moins de k0 étapes)
A1, ….. , An|-- C (en moins de k0 étapes)
L’hypothèse de récurrence donne que :
A1, ….. , An-1|— (An->(C->B))
A1, ….. , An-1|— (An->C)
Grâce à (SA2)
A1, ….. , An-1|-- ((An->(C->B))->((An->C)->(An->B))
((An->C)->(An->B)) par m.p
(An->B) par m.p
(e)B est obtenu par application de g. B = ∀ x C 7
 CALCUL DES PREDICATS DU 1er ORDRE
Soient A1, ……. , An-1, An des formules closes
Si A1, … , An-1, An |---- B alors A1, …… , An-1 |--- (An→B)

cas : B = ∀ x C g. (généralisation) : A |-- ∀x A

F1

(Ai)1≤i ≤n
SA5 : ((D → B) → (D → ∀x B))
C

Fk : B= ∀ x C
A1, …… , An-1 |--- (An→C)

gk0 : C
gk0+1 : ((An → C)
gk0+2 : ((An → C) → (An → ∀x C))
gk0+3 : (An → ∀x C)) soit (An → B)
8
 CALCUL DES PREDICATS DU 1er ORDRE

SEMANTIQUE

Une interprétation d’une fbf G est définie par les étapes suivantes :
➢Définir un domaine d’interprétation D i.e. un ensemble non vide
d’éléments qui sont les valeurs possibles des termes
➢Assigner à chaque constante de G un élément de D
➢Assigner à chaque prédicat d’arité n≥1 une application de Dn dans {V,F}
➢Assigner à chaque proposition une valeur dans {V,F}
➢Assigner à chaque fonction d’arité n≥1 une application de Dn dans D
On dit alors que G est interprétée sur D.

9
 CALCUL DES PREDICATS DU 1er ORDRE

TERMINOLOGIE
➢Un modèle d’une formule f est une interprétation i telle que i(f)=V
➢On appelle tautologie (ou thèse) toute formule A telle que pour toute
interprétation i , i(A)=V. On écrit alors |= A .
➢On dit que la formule B est conséquence de la formule A si pour toute
interprétation i telle que i(A)=V, on a aussi i(B)=V. On écrit alors A|= B
➢B est conséquence de ℘ (℘|= B) si pour toute interprétation i telle que pour
tout A de ℘ i(A)=V, on a aussi i(B)=V.
➢On dit qu’une formule A est satisfiable ou consistante s’il existe une
interprétation i telle que i(A)=V
➢On dit que l’ensemble des formules ℘ est satisfiable ou consistant s’il a un
10
modèle (insatisfiable ou inconsistante dans le cas contraire)
 CALCUL DES PREDICATS DU 1er ORDRE

PROPOSITIONS

Proposition4:
Soit A une formule
Si |-- A (i.e. théorème) alors |== A(tautologie)

Proposition5 (théorème de complétude):

Soit A une formule , Si |== A alors |-- A

Proposition6 (théorème de compacité):

Soit F un ensemble de formules.
Si toute famille finie F’ ⊂ F est satisfiable, alors F est satisfiable

11
 CALCUL DES PREDICATS DU 1er ORDRE

PROPOSITIONS

Proposition7 (théorème de finitude):

Soit F un ensemble de formules et B une fbf
Si F |= B alors il existe F’ ⊂ F , F’ fini, tel que : F’ |= B

Proposition8 (théorème de complétude généralisé):

Soit F un ensemble de formules et B une fbf
F |= B si et seulement si F |-- B

12
 CALCUL DES PREDICATS DU 1er ORDRE
EXERCICE

A |= B si et seulement si A ∪ {⎤ B} insatisfiable

➢Supposons que A |= B
Soit i une interprétation
Si i[a] = V pour tout a ∈ A alors i[B]=V. Donc i[⎤ B]=F et i n’est
pas modèle de A ∪ {⎤ B}
Si i[a] = F pour un a ∈ A alors i n’est pas modèle de A ∪ {⎤ B}

➢Supposons que A ∪ {⎤ B} soit insatisfiable

Soit i telle que i[a]=V pour tout a de A
Puisque A ∪ {⎤ B} n’a pas de modèle, il est impossible que i[⎤ B]
soit V donc i[B]=V
13
 CALCUL DES PREDICATS DU 1er ORDRE

EXERCICE

F |-- ⎤B si F n’a pas de modèle où B tautologie

Si F |-- ⎤B alors F |= ⎤ B, donc à chaque fois que i[A]=V pour

tout A ∈ F, on a i[⎤ B]=V. Comme pour toute interprétation i

on a i[B]=V, on voit qu’il ne peut exister de i tel que i[A]=V

pour tout A de F i.e. F n’a pas de modèle.

14
 CALCUL DES PREDICATS DU 1er ORDRE

FORMES NORMALES

➢Un littéral est une formule sous la forme X ou ⎤X où X est

un atome

➢Une clause est une disjonction de littéraux

➢On appelle forme normale conjonctive toute formule de la

forme G = ˄i=1..n Hi où Hi est une disjonction finie de littéraux

➢On appelle forme normale disjonctive toute formule de la

forme G = vi=1..n Hi où Hi est une disjonction finie de littéraux

15
 CALCUL DES PREDICATS DU 1er ORDRE

FORMES NORMALES PRENEXE

Une fbf G est une forme normale prénexe ssi G s’écrit sous
la forme suivante : G = (Q1 x1 . . .Qnxn) M
où Qi = ∃ ou ∀
et M est une fbf sans quantificateur dite matrice

Exemple : (∀x)( ∃y)( ∃z) P(x,y) !H(x,z)

16
CALCUL DES PREDICATS DU 1er ORDRE

FORMES EQUIVALENTES

F !G ≡ ⎤FvG
⎤ F ! G ≡ FvG
⎤(F ! ⎤G) ≡ F^G
F↔G ≡ (⎤F^⎤G)v(F^G)
⎤(⎤G) ≡ G
⎤ (AvB) ≡ ⎤A^⎤B
⎤ (A^B) ≡ ⎤Av⎤B
⎤ (∀xP(x)) ≡ ∃x ⎤P(x)
⎤ (∃xP(x)) ≡ ∀x⎤P(x)
17
CALCUL DES PREDICATS DU 1er ORDRE

ORDRE DES QUANTIFICATEURS

∀x ∃y (x>y) ⇒ y est fonction de x

∃x ∀y (x>y) ⇒ y est indépendant de x

18
 CALCUL DES PREDICATS DU 1er ORDRE
∀x ∃y (x>y) ⇒ y est fonction de x
FORME DE SKOLEM ∃x ∀y (x>y) ⇒ y est indépendant de x

Soit Q1x1 ….Qmxm B(x1, x2, ….,x) une formule A mise sous forme
prénexe.
On appelle forme de Skolem de A et on note AS la formule obtenue en
enlevant tous les quantificateurs ∃xi, en remplaçant chacune des
variables xi quantifiée avec un ∃ par fi (xj1, xj2, …, xjl) où xj1, xj2, …, xjl
sont les variables quantifiées par des ∀ placés avant le ∃xi. On
suppose bien sûr que tous les fi introduits sont différents de tous ceux
par ailleurs. Lorsqu’il n’y a aucun quantificateur ∀ devant le ∃ xi, le
symbole que l’on introduit est une constante.
A = ∀x p(x)˄∃ y q(y) 19
 CALCUL DES PREDICATS DU 1er ORDRE

EXEMPLES

Formule Forme de Skolem

∃ x p(x,f(x)) p(a,f(a))

∀ x ∃ y p(x,f(y)) ∀ x p(x,f(f1(x)))

∃ x1 ∀ x2 ∃ x3 ∃ x4 (p(x1,x2) → r(x3,x4)) ∀ x2 (p(a,x2)→ r(f1(x2),f2(x2)))

∃ x1 ∀x2 ∃ x3 ∀ x4 ∃ x5 p(x1,x2,x3,x4,x5) ∀ x2 ∀ x4 p(a,x2,f1(x2),x4,f2(x2,x4))

20
 CALCUL DES PREDICATS DU 1er ORDRE
Méthode de transformation d'une fbf en fnp

1. Eliminer les connecteurs → et <->

(G <−> F) ≡ (G → F) ∧ (F → G)
(G → F) ≡ (¬G ∨ F)
2. Accoler les connecteurs ¬ aux atomes concernés
¬(¬G) ≡ G
¬(F∨ G) ≡ ¬F ∧ ¬G
¬(F∧ G) ≡ ¬F ∨ ¬G
¬((∀X) P(X)) ≡ (∃X) ¬P(X)
¬((∃X) P(X)) ≡ (∀X) ¬P(X)
3. Rebaptiser les variables liées si nécessaire de sorte que chaque quantificateur
gouverne une variable originale
(∀X) P(X) ≡ (∀Y) P(Y)
(∃X) P(X) ≡ (∃Y) P(Y)
4. Déplacer tous les quantificateurs à gauche de la formule (sans changer l'ordre
relatif)
((Q1 X) F(X)) ∨ ((Q2 Y) H(Y)) ≡ (Q1 X) (Q2 Y) (F(X) ∨ (H(Y))
((Q1 X) F(X)) ∧ ((Q2 Y) H(Y)) ≡ (Q1 X) (Q2 Y) (F(X) ∧ (H(Y)) 21
CALCUL DES PREDICATS DU 1er ORDRE
Exercices skolémisation

(∃X (P(X) → Q(X))) → (∀X P(X) → ∃X Q(X))

≡ (¬(∃X (P(X) → Q(X))) ∨ ((∀X) P(X) → ∃X Q(X))
≡ (¬(∃X (¬P(X) ∨ Q(X))) ∨ ((¬(∀X P(X))) ∨ ∃X Q(X))
≡ (∀X (P(X) ∧ ¬Q(X))) ∨ (∃X (¬P(X)) ∨ ∃X Q(X))
≡ (∀X (P(X) ∧ ¬Q(X))) ∨ (∃X (¬P(X) ∨ Q(X)))
≡ (∀X (P(X) ∧ ¬Q(X))) ∨ (∃Y (¬P(Y) ∨ Q(Y)))
≡ ∀X ∃Y ((P(X) ∧ ¬Q(X)) ∨ (¬P(Y) ∨ Q(Y)))

(∀X) P(X) → (∃X) Q(X)

≡ (¬((∀X) P(X))) ∨ (∃X) Q(X)
≡ (∃X) ¬P(X)) ∨ (∃X) Q(X)
≡ (∃X) (¬P(X) ∨ Q(X))

22
 CALCUL DES PREDICATS DU 1er ORDRE

THEOREME DE SKOLEM

Proposition9:
✓Soit {A1, A2, …, An} un ensemble fini de formules du calcul des
prédicats
✓Soit {A1S, A2S, …, AnS } l’ensemble des formules de Skolem de
ces formules

{A1, …., An} admet un modèle de domaine E

si et seulement si
{A1S, A2S, …, AnS }admet un modèle de domaine E

23
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION

Démontrer que la formule T est conséquence de A est équivalent à

démontrer que : A U{⎤T} n’a pas de modèle
On est donc ramené au problème de savoir si un certain ensemble de
formules F0 possède des modèles ou non. Pour résoudre un tel
problème, on procède de la manière suivante :
✓Mise sous forme prénexe des formules de F0 ⇒ F1
✓Mise sous forme de Skolem des formules de F1 ⇒ F2
✓Suppression des quantificateurs universels de F2 ⇒ F3
✓Mise sous forme de clauses des formules de F3 ⇒ F4
Existence de modèles pour F0 équivalent à l’existence des modèles
pour chaque Fi en particulier F4 24
 CALCUL DES PREDICATS DU 1er ORDRE

EXEMPLE

Soit T = ∃ x ∃ y q(x , y) et A = {∀x (p(x) → ∃ y (r(y) ˄ q(x,y))) , ∃ x p(x)}

A |= T ?

F0 = {∀x (p(x) → ∃ y (r(y) ˄ q(x,y))) , ∃ x p(x), ⎤ ∃ x ∃ y q(x , y) }

F1 : Mise sous forme Prenexe F3 : Suppression des ∀

F1={∀x ∃ y (⎤p(x) v (r(y) ˄ q(x,y))), F3 ={(⎤ p(x) v (r(f(x)) ˄q(x,f(x)))),
∃ x p(x), p(a),
∀ x ∀ y ⎤ q(x , y) } ⎤ q(x , y) }

F2 : Mise sous forme Skolem F4 : Mise sous forme clauses

F2 ={∀x (⎤ p(x) v (r(f(x)) ˄ q(x,f(x)))) , F4 = {⎤ p(x) v q(x,f(x)) ,
p(a), ⎤ p(x) v r(f(x)),
∀ x ∀ y ⎤ q(x , y) } p(a),
⎤ q(x , y) } 25
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION
A priori, pour savoir si un ensemble de formules du calcul des
prédicats du premier ordre admet un modèle il faut réaliser une
infinité d’essais : essayer s’il y a un modèle ayant un domaine à
un élément, deux éléments, …, essayer s’il y a un modèle ayant
un domaine à une infinité d’éléments. Chacun de ces essais se
divise lui même en un très grand nombre d’essais.

L’intérêt du théorème de Herbrand est qu’il permet de se

ramener à un seul essai.
26
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION

Univers de Herbrand :
On appelle univers de Herbrand associé à {A1, …, An} et on

note U{A1, …, An} l’ensemble de tous les termes sans variables

construits à partir du vocabulaire des formules de {A1, …, An}.

De manière à n’avoir jamais d’univers de Herbrand vide,

lorsque ce vocabulaire ne contient pas de constante, on en
introduit une.
27
 CALCUL DES PREDICATS DU 1er ORDRE

EXEMPLE

A1 = ⎤ p(x) v q(x,f(x))

A2 = ⎤ p(x) v r(f(x))

A3 = p(a),

A4 = ⎤ q(x , y)

U{A1, …, A4} = {a, f(a), f(f(a)), ……. , f(f(….a)…)),…..}

N.B : Dès qu’il y a un symbole fonctionnel l’univers de Herbrand est infini

28
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION

Atomes de Herbrand
On appelle atomes de Herbrand associés à {A1, …, An} et on

note A{A1, …, An} l’ensemble de tous les atomes sans variables

construits à partir du vocabulaire des formules de {A1, …, An},

c’est à dire de toutes les formules de la forme p(t1,t2, .., tr) où

p est un symbole de prédicat de l’une des formules A1, A2, …,

An et où t1, t2, …, tr sont des éléments de U{A1, …, An}

29
 CALCUL DES PREDICATS DU 1er ORDRE

EXEMPLE

A1 = ⎤ p(x) v q(x,f(x))

A2 = ⎤ p(x) v r(f(x))

A3 = p(a),

A4 = ⎤ q(x , y)

A{A1, A2, A3, A4} = {p(a), r(a), q(a,a), p(f(a)), r(f(a)), q(a,f(a)), q(f(a),f(a)),

p(f(f(a))), ……}
U{A1, …, A4} = {a, f(a), f(f(a)), ……. , f(f(….a)…)),…..}

On écrit d’abord les atomes n’utilisant que le terme a; puis ceux utilisant en plus, le
terme f(a); puis ceux utilisant en plus, le terme f(f(a)); etc ….
30
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION
Système de Herbrand

On appelle système de Herbrand associé à {A1, …, An} et on

note S{A1, …, An} l’ensemble de toutes les formules obtenues à

partir des Ai en remplaçant dans les Ai les variables par des

éléments de l’univers de Herbrand. Lorsque les Ai sont des

clauses, les formules du système de Herbrand sont toutes

des disjonctions d’atomes de Herbrand et de négations
d’atomes de Herbrand 31
 CALCUL DES PREDICATS DU 1er ORDRE

EXEMPLE
A1 = ⎤ p(x) v q(x,f(x))

A2 = ⎤ p(x) v r(f(x))

A3 = p(a),

A4 = ⎤ q(x , y)
U{A1, A2, A3, A4} = {a, f(a), f(f(a)), ……. , f(f(….a)…)),…..}

Comme pour les atomes de Herbrand, on écrit d’abord les formules obtenues à partir de
A1, A2, A3, A4 en substituant a aux variables; puis celles obtenues en substituant a ou

f(a) aux variables; etc ….

S{A1, A2, A3, A4} = {⎤ p(a) v q(a,f(a)), ⎤ p(a) v r(f(a)), p(a), ⎤ q(a,a),

⎤p(f(a)) v q((f(a)),f((f(a))),⎤ p(f(a)) v r(f(f(a))), ⎤ q(a,f(a)),

⎤q(f(a),a),⎤q(f(a),f(a)), …..} 32
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION
Proposition10 : (théorème de Herbrand)
Soit {A1, …, An} un ensemble fini de clauses.
Les trois affirmations suivantes sont équivalentes :
✓{A1, …, An} possède un modèle
✓{A1, …, An} possède un modèle dont le domaine est l’univers
de Herbrand U{A1, …, An}
✓Le système de Herbrand S{A1, …, An} considéré comme un
ensemble de formules du calcul propositionnel dont les atomes
sont A{A1, …, An} possède un modèle
33
 CALCUL DES PREDICATS DU 1er ORDRE

PRINCIPE DE RESOLUTION

On numérote les formules de S{A1, …, An} = {F0, …, Fm, …..}

Proposition 11 :
L’ensemble {A1, …, An} n’admet pas de modèle si et

seulement si une des formules F0^F1^…..^Fm est insatisfiable

34