Formalismes de Représentation et Raisonnements

Exercices et exemples de cours

1 Chaînages
Soient les bases de règles et de faits suivantes :
Base de règles :
R1 : si Bénédicte et Denis et Etienne viennent alors Farida vient
R2 : si Gérard et Denis viennent alors Amélie vient
R3 : si Coralie et Farida viennent alors Amélie vient
R4 : si Bénédicte vient alors Xavier vient
R5 : si Xavier et Amélie viennent alors Herman vient
R6 : si Coralie vient alors Denis vient
R7 : si Xavier et Coralie viennent alors Amélie vient
R8 : si Xavier et Bénédicte viennent alors Denis vient
Base de faits = {Bénédicte , Coralie}
1. Est-ce que les règles de la base de régles sont sous forme de clause de Horn ?
2. Saturer la base de faits avec les règles en suivant l’algorithme de chaînage avant (on déter-
mine quelles sont les personnes à inviter absolument si Bénédicte et Coralie sont invitées).
3. Herman fait-il partie de la base de faits saturée ?
 Formalismes de Représentation et Raisonnements

Exercices et exemples de cours (2)

2 Chaînage Arrière
On considère l’algorithme de chaînage arrière ci-dessous. Cet algorithme peut boucler dans
certains cas. Donner un exemple de tels cas et modifier l’algorithme de façon à ce que son arrêt
soit assuré (tout en gardant sa correction !).

Algorithme BC(K,Q) // chaînage arrière

// Donnée : K = (BF,BR) et Q une liste d’atomes
// Remarque : on voit un fait A comme une règle -> A (hypothèse vide)
// Résultat : vrai ssi Q peut être produit par application
// des règles de BR sur BF (mais l’ algorithme
// peut ne pas s’arrêter)

Début
Si Q = vide alors retourner vrai
Pour toute règle R = H1 /\ ... /\ Hn -> C de BR et BF
telle que C = premier(Q)
// premier(Q) = premier atome de la liste Q
Q’ <- Concaténer [H1 ... Hn] et reste(Q)
// reste(Q) = Q privé de son 1er atome
Si BC(K,Q’) = vrai alors retourner vrai
FinPour
Retourner faux
Fin

3 Écriture en LPO
Traduire les énoncés ci-dessous en LPO en utilisant les symboles de prédicats suivants :
m(x) : x est méchant
chat(x) : x est un chat
a(x, y) : x aime y
co(x, y) : x connait y
p(x) : x est une personne
1. Il existe une personne méchante.
2. Il n’existe pas de personne méchante.
 3. Toutes les personnes sont méchantes.
4. Seules les personnes sont méchantes.
5. Les personnes qui aiment les chats ne sont pas méchantes.
6. Toute personne aime quelqu’un et personne n’aime tout le monde, ou bien quelqu’un aime
tout le monde et quelqu’un n’aime personne.
7. Il y a des personnes qui n’aiment pas les chats.

4 Modèles
Soit le langage L construit sur {a, P, f } où a est une constante, P un prédicat binaire et f une
fonction unaire. Proposer un ou plusieurs modèles pour chacune des formules suivantes :


1. F = ∀x∀y P (x, y) ∨ P (y, x)
2. G = ∀x P (x, f (x))


3. H = ∀x∀y P (x, f (y)) → P (x, y)
 Formalismes de Représentation et Raisonnements

Devoir Maison facultatif (à rendre pour le 02/03/2020)

1 Chaînages
Soient les bases de règles et de faits suivantes :
Base de règles :
R1 : si Pierre vient, alors Juliette vient
R2 : si Laurine et Maria viennent, alors Pierre vient
R3 : si Titouan et Laurine viennent, alors Maria vient
R4 : si Nicolas et Pierre viennent, alors Laurine vient
R5 : si Nicolas et Titouan viennent, alors Laurine vient
Base de faits = {Nicolas, Titouan} (On sait que Nicolas et Titouan viennent.)
1. Est-ce que les règles de la base de règles sont sous forme de clause de Horn ?
2. Laurine fait-elle partie de la base de faits saturée en suivant l’algorithme de chaînage avant ?
3. Montrer que Juliette vient en suivant l’algorithme de chaînage avant.

2 Écriture en logique du premier ordre

Soient les propositions suivantes :
a. Tous les invités ont pris au moins un fromage ou un dessert.
b. Tous les invités qui ont pris un dessert ont pris un café.
c. Les invités qui ont pris un café n’ont pas tous pris un dessert.
Traduire ces suppositions en logique des prédicats en utilisant les symboles de prédicats suivants :
f (x) (x a pris du fromage), d(x) (x a pris du dessert), c(x) (x a pris du café).

3 Substitutions

 

Soit F = ∀x u h(x, y), g(y), z ∨ ∀y∃z v(y, z) → w(x, y, z) .
1. Quelles sont les variables libres de F ?
2. F [f (x, y, z)/x] ?
3. F [t(x, y)/y]
4 Algorithme d’unification
Soient s = f (a, x, h(g(z))) et t = f (z, h(y), h(y)) deux termes, avec x, y, z, a des variables
du langage prédicatif.
1. Appliquer l’algorithme d’unification à U = {s, t}. Dérouler l’algorithme de manière dé-
taillée ; en particulier, rédiger entièrement la justification pour les étapes association et
fusion.
2. Si l’exécution de l’algorithme indique que s et t sont unifiables, écrire le résultat de sσ et
tσ (où tσ est l’application de la substitution σ au terme t).
3. Conclure.
Soient s = f (g(x), g(y), z) et t = f (z, x, g(a)) deux termes, avec x, y, z, a des variables du
langage prédicatif.
1. Appliquer l’algorithme d’unification à U = {s, t}. Dérouler l’algorithme de manière dé-
taillée ; en particulier, rédiger entièrement la justification pour les étapes association et
fusion.
2. Si l’exécution de l’algorithme indique que s et t sont unifiables, écrire le résultat de sσ et
tσ (où tσ est l’application de la substitution σ au terme t).
3. Conclure.
Soient s = f (g(v), h(u, v)) et t = f (g(w), h(w, j(x, w))) deux termes, avec u, v, w, x des va-
riables du langage prédicatif.
1. Appliquer l’algorithme d’unification à U = {s, t}. Dérouler l’algorithme de manière dé-
taillée ; en particulier, rédiger entièrement la justification pour les étapes association et
fusion.
2. Écrire le résultat de sσ et tσ , où tσ est l’application de la substitution σ (construite lors de
l’exécution de l’algorithme) au terme t.
3. Conclure : s et t sont-ils unifiables ?
 Formalismes de Représentation et Raisonnements

Règles d’inférence de la déduction naturelle

Axiome :
Ax
Γ, p ` p
Introduction de la négation :
Γ, p `⊥
¬I
Γ ` ¬p
Élimination de la négation :
Γ`p Γ ` ¬p
¬E
Γ `⊥
Ab absurdo :
Γ, ¬p `⊥
Abs
Γ`p
Élimination du faux (ex falso) :
Γ `⊥
⊥E
Γ`p
Introduction de l’implication :
Γ, p ` q
→I
Γ`p→q
Élimination de l’implication (modus ponens) :
Γ`p→q Γ`p
→E
Γ`q
Introduction du et :
Γ`p Γ`q
∧I
Γ`p∧q
Élimination du et à gauche (attention, on garde la gauche) :
Γ`p∧q
∧Eg
Γ`p
Élimination du et à droite (attention, on garde la droite) :
Γ`p∧q
∧Ed
Γ`q
Introduction du ou à gauche (attention, on introduit à droite) :
Γ`p
∨Ig
Γ`p∨q
Introduction du ou à droite (attention, on introduit à gauche) :
Γ`q
∨Id
Γ`p∨q
Élimination du ou :
Γ`p∨q Γ, p ` r Γ, q ` r
∨E
Γ`r
Introduction du quantificateur universel :

Γ`F
∀I si x n’est pas libre dans Γ
Γ ` ∀x F

Élimination du quantificateur universel :

Γ ` ∀x F (x)
∀E
Γ ` F [t/x]
Introduction du quantificateur existentiel :

Γ ` F (t)
∃I
Γ ` ∃x F (x)

Élimination du quantificateur existentiel :

Γ ` ∃x F Γ`F →G
∃E si x n’est pas libre dans Γ et G
Γ`G
 Formalismes de Représentation et Raisonnements

Révisions

1 Logique propositionnelle
1. Les formules suivantes sont-elles valides ? Justifier.
(a) (B → A) → (A ∨ B)
(b) (A ∧ B ∧ ¬C) ∨ ((A ∧ B) → C)
2. Mettre les formules précédentes sous forme normale conjonctive.
3. Soient les bases de règles et de faits suivantes :
Base de règles :
R1 : si Alice vient, alors Claude vient
R2 : si Benjamin et Claude viennent, alors Émilie vient
R3 : si Alice et Benjamin et Émilie viennent alors Dominique vient
R4 : si Claude et Dominique et Émilie viennent alors Fred vient
Base de faits = {Alice, Benjamin}
(a) Est-ce que les règles de la base de règles sont sous forme de clause de Horn ?
(b) Saturer la base de faits avec les règles en suivant l’algorithme de chaînage avant.
(c) Fred fait-il partie de la base de faits saturée ?

2 Unification
Soient s = f (a, x, h(g(z))) et t = f (z, h(y), h(y)) deux termes, avec x, y, z, a des variables
du langage prédicatif.
1. Appliquer l’algorithme d’unification à U = {s, t}. Dérouler l’algorithme de manière dé-
taillée ; en particulier, rédiger entièrement la justification pour les étapes association et
fusion.
2. Si l’exécution de l’algorithme indique que s et t sont unifiables, écrire le résultat de sσ et
tσ (où tσ est l’application de la substitution σ au terme t).
3. Conclure.
3 Déduction naturelle
1. A l’aide des règles de la déduction naturelle, montrer les postulats suivants :
(a) (p ∧ q) ∧ r, s ∧ t ` q ∧ s
(b) ¬(p ∨ q) ` ¬p ∧ ¬q
2. Soient les suppositions suivantes :
i. Tous les invités ont pris au moins un fromage ou un dessert.
ii. Tous les invités qui ont pris un dessert ont pris un café.
iii. Les invités qui ont pris un café n’ont pas tous pris un dessert.
(a) Traduire ces suppositions en logique des prédicats en utilisant les symboles de prédicats
suivants : f (x) (x a pris du fromage), d(x) (x a pris du dessert), c(x) (x a pris du café).
(b) Peut-on en conclure que certains invités ont pris du fromage ? un dessert ? Donner une
preuve en déduction naturelle, lorsque c’est possible.

4 Résolution en logique des prédicats

Soient les prédicat p, q, r, s d’arité 1 et des variables ’x’, ’y’, ’z’. On définit les formules sui-
vantes :

φ1 = ∃x p(x) ∧ q(x)
φ2 = ∀y p(y) → (r(y) ∧ s(y))
φ = ∃z q(z) ∧ s(z)

Montrer que φ1 , φ2 ` φ.
Annexes
Algorithme: Chainage_avant (BF (base de faits), BR (base de règles (R)), F (fait que l’on
cherche à établir))

tant que (F ∈BF)

/ ET (∃ R ∈ BR applicable) faire
— Choisir une règle applicable R
— BR = BRS -R désactivation de R
— BF = BF conclusion(R) déclenchement de la règle R,
conclusion de R ajoutée à la base de faits
si F ∈ BF alors
F est établi
sinon
F n’est pas établi

Entrée : ensemble de couples de termes à unifier U (récursivité !).

Soient (s, t) ∈ U et σ l’unificateur en construction :
suppression Si s = t, on les supprime de U.
décomposition Si s = f (s1 , ..., sn ) et t = f (t1 , ..., tn ), on supprime le couple de U, et on y ajoute les
couples (s1 , t1 ), ..., (sn , tn ).
association Si s = x (et t 6= x), et :
— x n’est pas déjà modifié par σ,
— x n’apparaît pas dans tσ
alors on met à jour σ par σ[tσ/x] (de même en inversant s et t)
fusion Si s = x (et t 6= x), et x est modifié par σ, on remplace le couple à unifier (x, t) par (σ(x), t).
Si aucune étape ne peut s’appliquer, les termes ne sont pas unifiables.

Règle de résolution en logique des prédi-

La formule se transforme en cats :
¬(∀x. φ) ∃x. ¬φ ¬p ∨ L1 ∨ . . . ∨ Lm p ∨ M1 ∨ . . . ∨ Mn
¬(∃x. φ) ∀x. ¬φ L1 ∨ . . . ∨ Lm ∨ M1 ∨ . . . ∨ Mn
φ ∨ ∀x. φ0 ∀x0 . (φ ∨ φ0 [x0 /x])
φ ∨ ∃x. φ0 ∃x0 . (φ ∨ φ0 [x0 /x])
(∀x. φ) ∨ φ0 ∀x0 . (φ[x0 /x] ∨ φ0 )
(∃x. φ) ∨ φ0 ∃x0 . (φ[x0 /x] ∨ φ0 )
φ ∧ ∀x. φ0 ∀x0 . (φ ∧ φ0 [x0 /x])
φ ∧ ∃x. φ0 ∃x0 . (φ ∧ φ0 [x0 /x])
(∀x. φ) ∧ φ0 ∀x0 . (φ[x0 /x] ∧ φ0 )
(∃x. φ) ∧ φ0 ∃x0 . (φ[x0 /x] ∧ φ0 )
φ → ∀x. φ0 ∀x0 . (φ → φ0 [x0 /x])
φ → ∃x. φ0 ∃x0 . (φ → φ0 [x0 /x])
(∀x. φ) → φ0 ∃x0 . (φ[x0 /x] → φ0 )
(∃x. φ) → φ0 ∀x0 . (φ[x0 /x] → φ0 )
 Formalismes de Représentation et Raisonnements

Algorithme d’unification – un exemple

Énoncé : Soient f, g, h, n des symboles de fonctions et x, y, z, v des variables. Écrire l’exécution

de l’algorithme d’unification sur les termes suivants :



s = f h(x, y), g(x) et t = f h(n(y), h(z, z)), v
n o n
o
Résolution : U est une file. On commence avec U = s, t = f h(x, y), g(x)), f (h(n(y), h(z, z)), v
et σ = [ ].
n

o
σ=[] U= f h(x, y), g(x) , f h(n(y), h(z, z)), v



On ne peut pas
appliquer suppression,
car f h(x, y), g(x) 6
= f h(n(y), h(z, z)), v . Comme
f h(x, y), g(x) et f h(n(y), h(z, z)), v sont le résultat de l’application de la même fonction f
au même nombre d’arguments (2 arguments), on peut appliquer la décomposition.



1 – Décomposition On supprime f h(x, y), g(x) , f h(n(y), h(z, z)), v de U. On ajoute
   
dans U les couples h(x, y), h(n(y), h(z, z)) et g(x), v .
n
  o
σ=[] U= h(x, y), h n(y), h(z, z) , g(x), v


On s’intéresse maintenant au premier couple présent dans U : h(x, y), h n(y), h(z, z) . On ne


peut pas appliquer

suppression, car h(x, y) 6
= h n(y), h(z, z) . Comme h(x, y) et
h n(y), h(z, z) sont le résultat de l’application de la même fonction h au même nombre d’argu-
ments (2 arguments), on peut appliquer la décomposition.


2 – Décomposition On supprime h(x, y), h n(y), h(z, z) de U. On ajoute dans U les couples
   
x, n(y) et y, h(z, z) . Comme U est modélisé par une file, on ajoute les nouveaux couples à la
suite des couples déjà présents dans U (on ajoute donc « par la droite »).
n     o
σ=[] U= g(x), v , x, n(y) , y, h(z, z)
 
On s’intéresse maintenant au premier couple présent dans U : g(x), v . On ne peut pas appliquer
suppression, car g(x) 6= v. On ne peut pas appliquer décomposition car g(x) est le résultat
de l’application de la fonction g alors que v est une variable. Comme v est une variable, g(x) 6= v,
v n’est pas déjà modifié par σ (car σ = [ ]), et v n’apparait pas dans σ(g(x)) = g(x), on peut
appliquer association.
3 – Association On met à jour σ par [σ(g(x))/v] ◦ σ.

σ := [σ(g(x))/v] ◦ σ = [g(x)/v] ◦ [ ] = [g(x)/v]

 
On supprime le couple g(x), v de U, puis on met à jour U en appliquant le nouveau σ.
n o n   o
U = σ(x, n(y)), σ(y, h(z, z)) = x, n(y) , y, h(z, z)
 
On s’intéresse maintenant au premier couple présent dans U : x, n(y) . On ne peut pas appli-
quer suppression, car x 6= n(y). On ne peut pas appliquer décomposition car n(y) est
le résultat de l’application de la fonction n alors que x est une variable. Comme x est une va-
riable, n(y) 6= x, x n’est pas déjà modifié par σ, et x n’apparait pas dans σ(n(y)) = n(y), on peut
appliquer association.

4 – Association On met à jour σ par [σ(n(y))/x] ◦ σ.

σ := [σ(n(y))/x] ◦ σ = [n(y)/x] ◦ [g(x)/v] = [g(n(y))/v, n(y)/x]

 
On supprime le couple x, n(y) de U, puis on met à jour U en appliquant le nouveau σ.
n o n o
U = σ(y, h(z, z)) = y, h(z, z)
 
On s’intéresse maintenant au premier couple présent dans U : y, h(z, z) . On ne peut pas appli-
quer suppression, car y 6= h(z, z). On ne peut pas appliquer décomposition car h(z, z) est
le résultat de l’application de la fonction h alors que y est une variable. Comme y est une variable,
h(z, z) 6= y, y n’est pas déjà modifié par σ, et y n’apparait pas dans σ(h(z, z)) = h(z, z), on peut
appliquer association.

5 – Association On met à jour σ par [σ(h(z, z))/y] ◦ σ.

σ := [σ(h(z, z))/y] ◦ σ = [h(z, z)/x] ◦ [g(n(y))/v, n(y)/x]

= [h(z, z)/y, g(n(h(z, z)))/v, n(h(z, z))/x]
 
On supprime le couple y, h(z, z) de U. U = ∅, ce qui termine l’exécution de l’algorithme.

Vérification
σ(s) = f (h(n(h(z, z)), h(z, z)), g(n(h(z, z))))
σ(t) = f (h(n(h(z, z)), h(z, z)), g(n(h(z, z))))
 Formalismes de Représentation et Raisonnements

Résolution en logique des prédicats – un exemple

Énoncé : Soit un prédicat « chemin » (c) d’arité 2, une fonction « voisin » (v) d’arité 1, les
variables ’a, x, y, z’, et une constante « ici » (i). On définit les formules suivantes :


φ1 = ∀x. c x, v(x)


φ2 = ∀x.∀y.∀z. c(x, z) ∧ c(z, y) → c(x, y)


φ = ∃a. c i, v v(a)

Montrer que φ1 , φ2 ` φ.

Résolution : Pour démontrer φ, on va raisonner par l’absurde : on va chercher à démontrer la

contraposée de φ (¬φ) et aboutir à une contradiction.

1 – Contraposée On s’intéresse donc aux formules suivantes :

φ1 = ∀x. c x, v(x)


φ2 = ∀x.∀y.∀z. c(x, z) ∧ c(z, y) → c(x, y)


¬φ = ∀a. ¬c i, v v(a)

En appliquant la règle de résolution en logique des prédicats, on cherche à aboutir à une contradic-
tion. Pour pouvoir appliquer cette règle, il faut mettre les formules sous forme normale.

2 – Mise sous forme normale

a) Mise sous forme prénexe La forme prénexe d’une formule F est une formule F 0 équivalente
telle que tous les quantificateurs soient regroupés au début de F 0 . φ1 , φ2 et ¬φ sont déjà sous
forme prénexe.

b) Mise sous forme normale de Skolem La forme normale de Skolem d’une formule F est
une formule F 0 telle que tous les quantificateurs soient regroupés au début de F 0 et sont tous des
quantificateurs universels (F 0 n’est pas nécessairement équivalente à F mais l’une est satisfiable
si et seulement si l’autre l’est). φ1 , φ2 et ¬φ sont déjà sous forme normale de Skolem car tous
les quantificateurs qu’elles contiennent sont regroupés au début des formules et tous ces quantifi-
cateurs sont des quantificateurs universels.
c) Mise sous forme normale conjonctive φ1 est déjà sous forme normale conjonctive, il s’agit
d’une conjonction de disjonctions (0 conjonctions, 0 disjonctions).


 

φ2 = ∀x.∀y.∀z. c(x, z) ∧ c(z, y) → c(x, y) ≡ ∀x.∀y.∀z. ¬ c(x, z) ∧ c(z, y) ∨ c(x, y)
 
≡ ∀x.∀y.∀z. ¬c(x, z) ∨ ¬c(z, y) ∨ c(x, y)

¬φ est déjà sous forme normale conjonctive, il s’agit d’une conjonction de disjonctions (0
conjonctions, 0 disjonctions). Voici les trois formules que l’on considère maintenant :

F1 = φ1 = ∀x. c x, v(x)
 
F2 = ∀x.∀y.∀z. ¬c(x, z) ∨ ¬c(z, y) ∨ c(x, y)


F3 = ¬φ = ∀a. ¬c i, v v(a)

On cherche à appliquer la règle de résolution en logique des prédicats pour combiner F1 , F2

et F3 et aboutir à une contradiction. Afin de pouvoir combiner les formules, il faut procéder à des
substituions judicieuses.

3 – Substitution et résolution Soit u une variable fraîche.

h i 


F2 i/x, v(v(u))/y = ∀u.∀z. ¬c(i, z) ∨ ¬c z, v(v(u) ∨ c i, v(v(u))

∀x disparait car la variable x est substituée par le terme i qui est une constante. ∀u vient remplacer
∀y puisque toutes les expressions dépendant de la variable y dépendent maintenant de la variable
u. h i 

F3 u/a = ∀u. ¬c i, v v(u)
On met ainsi en évidence la présence d’une sous-formule dans F2 , et de la négation de la même
sous-formule dans F3 :



F2 = ∀u.∀z. ¬c(i, z) ∨ ¬c z, v(v(u) ∨ c i, v(v(u))


F3 = ∀u. ¬c i, v v(u)

Par application de la règle de résolution aux résultats des substitutions :



∀u.∀z. ¬c(i, z) ∨ ¬c z, v(v(u)) = F4

On procède de même pour combiner F4 et F1 .

h i


F4 v(i)/z, i/u = ¬c i, v(i) ∨ ¬c v(i), v(v(i))
h i

F1 v(i)/x = c v(i), v(v(i))
Par application de la règle de résolution aux résultats des substitutions :


¬c i, v(i) = F5

On peut maintenant essayer de combiner F1 et F5 .

h i

F1 i/x = c i, v(i) ce qui contredit F5 .

On aboutit donc à une contradiction. Ainsi, φ1 , φ2 ` φ.

 Formalismes de Représentation et Raisonnements

Corrigé – Examen 2018

1 Logique propositionnelle
1.a)
p q r p→q (p → q) ∧ r ¬p ¬p ∧ r q∧r (p ∧ r) ∨ (q ∧ r)
0 0 0 1 0 1 0 0 0
1 0 0 0 0 0 0 0 0
0 1 0 1 0 1 0 0 0
0 0 1 1 1 1 1 0 1
1 1 0 1 0 0 0 0 0
1 0 1 1 0 1 0 0 0
0 1 1 1 1 1 1 1 1
1 1 1 1 1 0 0 1 1
La quatrième et la dernière colonne de la table de vérité sont identiques, ce qui prouve l’équi-
valence.

1.b)

 

(p → q) → p ∧ (q → r) → r ≡ (¬p ∨ q) → p ∧ (¬q ∨ r) → r

 

≡ ¬(¬p ∨ q) ∨ p ∧ (¬q ∨ r) → r ≡ ¬ (p ∧ ¬q) ∨ p ∧ (¬q ∨ r) ∨ r

 

≡ ¬ (p ∧ ¬q) ∨ p ∨ (¬q ∨ r) ∨ r ≡ ¬(p ∧ ¬q) ∧ ¬p ∨ (¬q ∨ r) ∨ r


≡ (¬p ∨ q) ∧ ¬p ∨ (¬q ∨ r) ∨ r


On pose P = (¬q∨r)∨r et Q∧R = (¬p∨q)∧¬p , puis on applique l’équivalence P ∨(Q∧R) ≡
(P ∨ Q) ∧ (P ∨ R).

   
≡ (¬p ∨ q) ∧ ¬p ∨ (¬q ∨ r) ∨ r ≡ (¬q ∨ r) ∨ r ∨ (¬p ∨ q) ∧ (¬q ∨ r) ∨ r ∨ ¬p

1.c) Une formule est valide si et seulement si pour toutes les interprétations, la formule est vraie.
 p q r ¬p ∨ q ¬q ∨ r (¬q ∨ r) ∨ r ∨ (¬p ∨ q) (¬q ∨ r) ∨ r ∨ ¬p
0 0 0 1 1 1 1
1 0 0 0 1 1 1
0 1 0 1 0 1 1
0 0 1 1 1 1 1
1 1 0 1 0 1 0
1 0 1 0 1 1 1
0 1 1 1 1 1 1
1 1 1 1 1 1 1

La formule est donc invalide car elle est fausse si p = 1, q = 1, r = 0.

2.a) Base de règles :

R1 : (C ∧ D) → F
R2 : (F ∧ B) → E
R3 : (G ∧ F ) → B
R4 : (A ∧ F ) → G

Base de faits : {A, C, D}.

Une clause de Horn est une clause comportant au plus un littéral positif ; une fois les équiva-
lences faites, toutes les règles de la base de règles sont de la forme ¬C ∨ ¬D ∨ F , donc comportent
un seul littéral positif.

2.b)

1 : R1 + C + D ⇒ F
2 : R4 + A + F ⇒ G
3 : R3 + G + F ⇒ B
4 : R2 + F + B ⇒ E

On arrive à déduire E en suivant l’algorithme de chaînage avant, donc Émilie vient.

2.c) À la fin de l’execution de l’étape 4, plus aucune règle ne peut être appliquée. La base de faits
{A, C, D, F, G, B, E} est donc saturée et G = Gaëlle en fait partie.

2 Logique du premier ordre

1 Représentation de F :
 ∃x

p ¬

x f ∀z

y q

z g

a t h

t
ERRATUM : dans la formule G, ∃y est en fait un ∃u. Cette erreur n’a pas beaucoup d’impact
sur le reste de l’exercice. La correction continue avec

G = r(x) ∨ ((∃u. ∀y. p(f (y), u) ∧ r(a)) ∧ ∀z. q(v, g(z, w, z)))

Représentation de G :
∨

r ∧

x ∃u ∀z

∀y q

∧ v g

p r z w z

f u a

2 Les variables colorées sont liées aux quantificateurs de la même couleur. Les variables libres
sont en noir et gras.

F = ∃x. p(x, f (y)) ∨ ¬∀z. q(z, g(a, t, h(t)))

G = r(x) ∨ ((∃u. ∀y. p(f (y), u) ∧ r(a)) ∧ ∀z. q(v, g(z, w, z)))

3 Pour F : p est un prédicat d’arité 2, f est une fonction d’arité 1, q est un prédicat d’arité 2, g
est une fonction d’arité 3, h est une fonction d’arité 1.
 Pour G : r est un prédicat d’arité 1, p est un prédicat d’arité 2, f est une fonction d’arité 1, q
est un prédicat d’arité 2, g est une fonction d’arité 3.
n o n

o
4 Résolution : On commence avec U = s, t = f g(v), h(u, v) , f g(w), h(w, j(x, w))
et σ = [ ].


On ne peut pas appliquer

suppression, car

f g(v), h(u, v) 6
= f g(w), h(w, j(x, w)) .
Comme f g(v), h(u, v) et f g(w), h(w, j(x, w)) sont le résultat de l’application de la même
fonction f au même nombre d’arguments (2 arguments), on peut appliquer la décomposition.



1 – Décomposition On supprime f g(v), h(u, v) , f g(w), h(w, j(x, w)) de U. On ajoute
   
dans U les couples g(v), g(w) et h(u, v), h(w, j(x, w)) .
n   o
σ=[] U= g(v), g(w) , h(u, v), h(w, j(x, w))
 
On s’intéresse maintenant au premier couple présent dans U : g(v), g(w) . On ne peut pas ap-
pliquer suppression, car g(v) 6= g(w). Comme g(v) et g(w) sont le résultat de l’applica-
tion de la même fonction g au même nombre d’arguments (1 argument), on peut appliquer la
décomposition.
   
2 – Décomposition On supprime g(v), g(w) de U. On ajoute dans U le couple v, w . Comme
U est modélisé par une file, on ajoute le nouveau couple à la suite des couples déjà présents dans
U (on ajoute donc « par la droite »).
n   o
σ=[] U= h(u, v), h(w, j(x, w)) , v, w
 
On s’intéresse maintenant au premier couple présent dans U : h(u, v), h(w, j(x, w)) . On ne peut
pas appliquer suppression, car h(u, v) 6= h(w, j(x, w)). Comme h(u, v) et h(w, j(x, w)) sont
le résultat de l’application de la même fonction h au même nombre d’arguments (2 arguments), on
peut appliquer la décomposition.
 
3 – Décomposition On supprime h(u, v), h(w, j(x, w)) de U. On ajoute dans U les couples
   
u, w et v, j(x, w) .
n     o
σ=[] U= v, w , u, w , v, j(x, w)
 
On s’intéresse maintenant au premier couple présent dans U : v, w . On ne peut pas appliquer
suppression, car v 6= w. Comme v et w ne sont pas le résultat de l’application de la même
fonction, on ne peut pas appliquer la décomposition. Comme v est une variable, w 6= v, v
n’est pas déjà modifié par σ (car σ = [ ]), et v n’apparait pas dans σ(w) = w, on peut appliquer
association.
4 – Association On met à jour σ par [σ(w)/v] ◦ σ.

σ := [σ(w)/v] ◦ σ = [w/v] ◦ [ ] = [w/v]

 
On supprime le couple v, w de U, puis on met à jour U en appliquant le nouveau σ.
n     n   o
U = σ u, w , σ v, j(x, w) } = u, w , w, j(x, w)
 
On s’intéresse maintenant au premier couple présent dans U : u, w . On ne peut pas appliquer
suppression, car u 6= w. Comme u et w ne sont pas le résultat de l’application de la même
fonction, on ne peut pas appliquer la décomposition. Comme u est une variable, w 6= u, u n’est
pas déjà modifié par σ, et u n’apparait pas dans σ(w) = w, on peut appliquer association.

5 – Association On met à jour σ par [σ(w)/u] ◦ σ.

σ := [σ(w)/u] ◦ σ = [w/u] ◦ [w/v] = [w/v, w/u]

 
On supprime le couple u, w de U, puis on met à jour U en appliquant le nouveau σ.
n   n o
U = σ w, j(x, w) } = w, j(x, w)
 
On s’intéresse maintenant au premier couple présent dans U : w, j(x, w) . On ne peut pas appli-
quer suppression, car w 6= j(x, w). Comme w et j(x, w) ne sont pas le résultat de l’applica-
tion de la même fonction, on ne peut pas appliquer la décomposition. Comme w apparait dans
σ(j(x, w)) = j(x, w), on ne peut pas appliquer association. Comme w n’est pas modifié par
σ, on ne peut pas appliquer fusion. Aucune étape ne peut s’appliquer ; les termes ne sont donc
pas unifiables.
3 Deduction naturelle
1

Ax Ax Ax Ax
Γ ` p → (q ∧ r) Γ`p Γ ` p → (q ∧ r) Γ`p
→E Γ`q∧r →E Γ`q∧r
∧I
∧Eg Γ = p → (q ∧ r), p ` q ∧Eg Γ = p → (q ∧ r), p ` q
→I →I
p → (q ∧ r) ` p → q p → (q ∧ r) ` p → q
p → (q ∧ r) ` (p → q) ∧ (p → r)

2
Ax Ax
∧Eg Γ ` (p → r) ∧ (q → r) ∧Eg Γ`p∧q
→E
→I Γ`p→r Γ`p
Γ = (p → r) ∧ (q → r), (p ∧ q) ` r
(p → r) ∧ (q → r) ` (p ∧ q) → r
4 Resolution en logique des predicats
Pour démontrer φ, on raisonne par l’absurde.

1 – Contraposée On s’intéresse donc aux formules suivantes :

φ1 = ∀x. p(x) → q(x, c)

φ2 = ∀x.∃y. ((r(x) ∨ ¬p(y)) → s(x, y))
φ3 = ∀x. p(x)


¬φ = ∃x. r(x) ∧ ∀y. ¬s(x, y) ∨ ¬b(y, c)

En appliquant la règle de résolution en logique des prédicats, on cherche à aboutir à une contradic-
tion. Pour pouvoir appliquer cette règle, il faut mettre les formules sous forme normale.

2 – Mise sous forme normale

a) Mise sous forme prénexe La forme prénexe d’une formule F est une formule F 0 équivalente
telle que tous les quantificateurs soient regroupés au début de F 0 . φ1 , φ2 et φ3 sont déjà sous
forme prénexe. En rouge et en bleu, la subdivision en sous-formules de ¬φ pour la mise sous
forme prénexe grâce au tableau des équivalences.


 

¬φ = ∃x. r(x) ∧ ∀y. ¬s(x, y) ∨ ¬b(y, c) ≡ ∃x. ∀z. r(x) ∧ ¬s(x, z) ∨ ¬b(z, c)

b) Mise sous forme normale de Skolem La forme normale de Skolem d’une formule F est une
formule F 0 telle que tous les quantificateurs soient regroupés au début de F 0 et sont tous des quan-
tificateurs universels. φ1 et φ3 sont déjà sous forme normale de Skolem.

φ2 : on définit une fonction f d’arité 1 qui fournit une valeur y = f (x) telle que

((r(x) ∨ ¬p(f (x))) → s(x, f (x)))

est vraie. On a alors :

∀x. ((r(x) ∨ ¬p(f (x))) → s(x, f (x)))

que l’on va appeler F2 . 

¬φ : on définit une constante k telle que ∀z. r(k) ∧ ¬s(k, z) ∨ ¬b(z, c) est vraie. On appelle
cette formule F4 .
c) Mise sous forme normale conjonctive φ3 est déjà sous forme normale conjonctive, il s’agit
d’une conjonction de disjonctions (0 conjonctions, 0 disjonctions).

φ1 = ∀x. p(x) → q(x, c) ≡ ∀x. ¬p(x) ∨ q(x, c)



F2 = ∀x. r(x) ∨ ¬p(f (x)) → s(x, f (x))


≡ ∀x. ¬ r(x) ∨ ¬p(f (x)) ∨ s(x, f (x))


≡ ∀x. ¬r(x) ∧ p(f (x)) ∨ s(x, f (x))



On pose P = s x, f (x) et Q∧R = ¬r(x)∧p f (x) , puis on applique l’équivalence P ∨(Q∧R) ≡
(P ∨ Q) ∧ (P ∨ R).

 


F2 = ∀x. s x, f (x) ∨ ¬r(x) ∧ s x, f (x) ∨ p f (x)

F4 est déjà sous forme normale conjonctive. On sépare F2 en F5 , F6 et F4 en F7 , F8 . Voici les

formules que l’on considère maintenant :

 
F1 = φ1 = ∀x. ¬p(x) ∨ q(x, c)
F3 = φ3 = ∀x. p(x)


F5 = ∀x. s x, f (x) ∨ ¬r(x)



F6 = ∀x. s x, f (x) ∨ p f (x)
F7 = ∀z. r(k)
 
F8 = ∀z. ¬s(k, z) ∨ ¬q(z, c)

On cherche à appliquer la règle de résolution en logique des prédicats pour combiner ces for-
mules et aboutir à une contradiction. Afin de pouvoir combiner les formules, il faut procéder à des
substituions judicieuses.

3 – Substitution et résolution Par application de la règle de résolution à F1 et F3 , on a :

∀x. q(x, c) = F9

Soit u une variable fraîche.

F9 [u/x] = ∀u. q(u, c)

 
F8 [u/z] = ∀u. ¬s(k, u) ∨ ¬q(u, c)

Par application de la règle de résolution on a :

∀u. ¬s(k, u) = F10

Maintenant :


F5 [k/x] = s k, f (k) ∨ ¬r(k)

Par application de la règle de résolution avec F7 on a :

s k, f (k)

Ce qui entre en contradiction avec F10 [f (k)/u] = ¬s(k, f (k)). Ainsi, φ1 , φ2 , φ3 ` φ.

 Formalismes de Représentation et Raisonnements

Substitutions – Exercices & corrigés

Exercice 1 Soit la formule de la logique des prédicats suivante :

H = ∀x.∀y. A(x, y) → B(x, y)

1. Pour chaque occurrence de variable, dire si elle est libre ou liée et dans le cas où elle est
liée, indiquer le quantificateur correspondant.
2. Donner tous les prédicats et toutes les fonctions, avec leurs arités, qui apparaissent dans la
formule.
3. Effectuer, étape par étape, la substitution H[f (x, y)/x].
4. Effectuer, étape par étape, la substitution H[f (x, y)/y].

Exercice 2 Soit la formule de la logique des prédicats suivante :

F = ∀x∃y R(f (x), f (y)) ∧ (∀z R(x, z)) → S(x)

1. Pour chaque occurrence de variable, dire si elle est libre ou liée et dans le cas où elle est
liée, indiquer le quantificateur correspondant.
2. Donner tous les prédicats et toutes les fonctions, avec leurs arités, qui apparaissent dans la
formule.
3. Effectuer, étape par étape, la substitution F [f (z)/x].
4. Effectuer, étape par étape, la substitution F [R(x, y)/z].

Exercice 3 Soit la formule de la logique des prédicats suivante :




G = ∀x. u h(x, y), g(y), z ∨ ∀y. ∃z. (v(y, z) → w(x, y, z))

1. Pour chaque occurrence de variable, dire si elle est libre ou liée et dans le cas où elle est
liée, indiquer le quantificateur correspondant.
2. Donner tous les prédicats et toutes les fonctions, avec leurs arités, qui apparaissent dans la
formule.
3. Effectuer, étape par étape, la substitution G[t(x, y)/y].
4. Effectuer, étape par étape, la substitution G[f (x, y, z)/x].
Correction – Exercice 1
3. On écrit H1 (x) où n’apparaît aucune occurence liée de x (la variable à substituer). On écrit
H2 (x) dont aucune variable liée n’apparait dans f (x, y) (le terme substitutant).


H1 (x) = ∀a.∀y. A(a, y) → B(x, y)


H2 (x) = ∀a.∀b. A(a, b) → B(x, y)


H[f (x, y)/x] = ∀a.∀b. A(a, b) → B(f (x, y), y)

4.


H[f (x, y)/y] = ∀a.∀b. A(a, b) → B(x, f (x, y))

Correction – Exercice 2
3.



F1 (x) = ∀a.∃y. R(f (a), f (y)) ∧ (∀z R(x, z)) → S(x)



F2 (x) = ∀a.∃y. R(f (a), f (y)) ∧ (∀b R(x, b)) → S(x)



F [f (z)/x] = ∀a.∃y. R(f (a), f (y)) ∧ (∀b R(f (z), b)) → S(f (z))

4.



F1 (z) = ∀x.∃y. R(f (x), f (y)) ∧ (∀a. R(x, a)) → S(x)

Il n’y a plus d’occurence libre de z. Donc F [R(x, y)/z] = F1 (z).

Correction – Exercice 3
3.



G1 (y) = ∀x. u h(x, y), g(y), z ∨ ∀a. ∃z. (v(a, z) → w(x, a, z))



G2 (y) = ∀b. u h(b, y), g(y), z ∨ ∀a. ∃z. (v(a, z) → w(b, a, z))



G[t(x, y)/y] = ∀b. u h(b, t(x, y)), g(t(x, y)), z ∨ ∀a. ∃z. (v(a, z) → w(b, a, z))

4.



G1 (x) = ∀a. u h(a, y), g(y), z ∨ ∀y. ∃z. (v(y, z) → w(a, y, z))

Il n’y a plus d’occurence libre de x. Donc G[f (x, y, z)/x] = G1 (x).

 Formalismes de Représentation et Raisonnements

Déduction naturelle – Exercices & corrigés

Exercice 1 Montrer, à l’aide des règles de la déduction naturelle :

∀x. (F (x) ∧ G(x)) ` (∀x. F (x)) ∧ (∀x. G(x))

Exercice 2 Montrer, à l’aide des règles de la déduction naturelle :

∀x. (F (x) → G(x)) ` ∀x. F (x) → (G(x) ∨ H(x))
Correction – exercice 1

Ax Ax
∀E Γ ` ∀x. (F (x) ∧ G(x)) ∀E Γ ` ∀x. (F (x) ∧ G(x))
∧Eg ∧Ed
∀I car x lié dans Γ Γ`F ∧G ∀I Γ`F ∧G
∧I
Γ`F Γ`G
Γ ` ∀x. F (x) Γ ` ∀x. G(x)
Γ = ∀x. (F (x) ∧ G(x)) ` (∀x. F (x)) ∧ (∀x. G(x))

Correction – exercice 2

Ax
∀E Γ, F ` ∀x. (F (x) → G(x)) Ax
→E Γ, F ` F
∨Ig Γ, F ` F → G
→I
∀I car x est lié dans Γ Γ, F ` G
Γ, F ` G ∨ H
Γ ` F → (G ∨ H)


Γ = ∀x. (F (x) → G(x)) ` ∀x. F (x) → (G(x) ∨ H(x))