Programmation Logique

GL3

1
Programmation Logique
 Introduction

2
Programmation Logique
 Classes de langages

n Langages impératifs
l séquencement des calculs spécifié
l syntaxe riche, mais peut-être lourde pour des
application IA
l exemples : Pascal, C, C+, C++, Java, …
n Langages fonctionnels:
l Basés sur la notion de fonction, reposent sur le -
calcul, forte utilisation de la récursivité
l exemples : Lisp, Scheme, Caml, …
n Langages logiques:
l Basés sur la logique, particulièrement la logique des
prédicats, forte utilisation de la récursivité, non
déterminisme
l Exemple: Prolog
3
Programmation Logique
 Historique

n 1930 Calcul des prédicats (J. Herbrand)

n 1965 Principe de résolution (J. A. Robinson)
n 1970 Utiliser la logique comme langage de
programmation
clauses de Horn R. Kowalski
n 1972 Premier interprète PROLOG (A. Colmerauer et P. Roussel)
Université d’Aix-Marseille
n 1977 Premier compilateur PROLOG (D. H. D. Warren)
Université d’Édimbourg
n 1980 Projet japonais de 5e génération

n 1990 PROLOG évolue vers la Programmation par Contraintes

4
Programmation Logique
 Bilan

PROLOG pour l’Industrie

n Prolog est utilisé pour

l prototyper très rapidement,

l tester des idées
l Et aussi pour développer des applications:
– Problèmes IA
– Problèmes combinatoires complexes (Prolog avec
contraintes): gestion de ressources, recherche
opérationnelle …

5
Programmation Logique
 Plan du cours

n Bases théoriques (La résolution en logique)

l Résolution en logique propositionnelle
– Rappels
– Formes normales
– Résolution
l Résolution en logique des prédicats
– Rappels
– Mise sous forme clausale
– Unification
– Résolution
n Le langage PROLOG
– Syntaxe
– Arbre de résolution
– Listes
– Coupe-choix
– Négation
– Arbres

6
Programmation Logique
 Références

n Bibliographie

l J. P. Delahaye, "Outils logiques pour l’intelligence artificielle",

Eyrolles, 1988.
l J. P Delahaye, "Cours de Prolog avec Turbo-Prolog", Eyrolles,
1988.
l F. Giannesini, H. Kanaoui, [Link], M. Van Caneghem,
"Prolog", InterEditions, 1985.

7
Programmation Logique
 La résolution en logique
propositionnelle

8
Programmation Logique
 I/ Rappels
n Syntaxe d’une formule

n Sémantique d’une formule

n Catégories de formules

n Formules équivalentes

9
Programmation Logique
 Calcul propositionnel

Exemple de formules équivalentes (à

retenir)

F  G  ( F  G )  (G  F )

F G  G F
( F  G )  F  G
(F )  F ( F  G )  F  G
lois de De Morgan
F  G  F  G

F G  G  F

10
Programmation Logique
 n

11
Programmation Logique
 Calcul propositionnel

II/Formes normales

n But avoir une représentation uniforme des

formules du calcul propositionnel

12
Programmation Logique
 Calcul propositionnel

Formes normales

n Une formule F est dite sous forme normale disjonctive ssi F est une
disjonction de conjonctions de variables propositionnelles et de négation
de variables propositionnelles

 i (pi1  pi2  ….  pin   p’i1   p’i2  ….   p’im)

n Une formule F est dite sous forme normale conjonctive ssi F est une
conjonction de disjonctions de variables propositionnelles et de
négation de variables propositionnelles

 i (pi1  pi2  ….  pin   p’i1   p’i2  ….   p’im)

n Théorème: Toute formule du calcul propositionnel est équivalente

à une formule sous forme normale disjonctive et à une formule
sous forme normale conjonctive

13
Programmation Logique
 III/ La résolution
n

14
Programmation Logique
 Calcul propositionnel

Validité du principe de résolution

n Il faut montrer que :

l  C’1 ,  l  C’2 ⊨ C’1  C’2

n Autrement dit, il faut montrer que:

si (l  C’1)  ( l  C’2 ) vrai alors (C’1  C’2 ) est aussi vrai

n Deux cas se présentent

l l est vrai
– nécessairement C’2 vrai et donc (C’1  C’2 ) aussi
l  l est vrai
– nécessairement C’1 vrai et donc (C’1  C’2 ) aussi

15
Programmation Logique
 La résolution sans variables (RSV)

16
Programmation Logique
 1. p1  p2 hyp
2.  p3  p2 hyp p1  p2  p1  p3
3.  p1  p3 hyp
4. p2  p3 Rés. 1 et 3
5. p2 Rés. 2 et 4
p2  p3  p3  p2

p2

17
Programmation Logique
 Propriétés de RSV
n

18
Programmation Logique
 n

19
Programmation Logique
 1. p1  p2 hyp
2.  p3  p2 hyp p1  p2  p1  p3
3.  p1  p3 hyp
4. p2  p3 Rés. 1 et 3
5. p2 Rés. 2 et 4
6.  p2 hyp p2  p3  p3  p2
7.  Rés. 5 et 6

 p2 p2

20
Programmation Logique
 La résolution en logique des
prédicats

21
Programmation Logique
 Calcul des prédicats

I/ Rappels

n Syntaxe
n Sémantique
n Catégories de formules
n Formules équivalentes
n Conséquence logique
n Renommage

22
Programmation Logique
 Exemples:
- x (p(x, f(x))  p(f(x),x)) n’est pas valide, mais elle est satisfiable
- ⊨ ∀𝑥 (𝑝 𝑥 ∨ ¬𝑝 𝑥 ) est une tautologie ou valide
- ∀𝑥 (𝑝 𝑥 ∧ ¬𝑝 𝑥 ) est insatisfiable
- ∀𝑥 ∀𝑦 𝑞 𝑥, 𝑦 ⇒ 𝑝 𝑥, 𝑦 , ∀𝑧 𝑞(𝑧, 𝑧) ⊨ ∀𝑧 𝑝(𝑧, 𝑧)
- L’ensemble de formules:
{x (p(a),
∀𝑥 𝑝 𝑥 ⇒ ¬𝑟 𝑥 ,

∀𝑦 ¬𝑟 𝑦 ⇒ 𝑞 𝑦 ,

∀𝑧 𝑞 𝑧 ⇒ ¬𝑝 𝑧 }
est insatisfiable ou inconsistant

23
Programmation Logique
 - x (p(x, f(x))  p(f(x),x)) n’est pas valide, mais elle est satisfiable

Pourquoi?

24
Programmation Logique
 - ⊨ ∀𝑥 (𝑝 𝑥 ∨ ¬𝑝 𝑥 ) est une tautologie ou valide

Pourquoi?

25
Programmation Logique
 - ∀𝑥 (𝑝 𝑥 ∧ ¬𝑝 𝑥 ) est insatisfiable

Pourquoi?

26
Programmation Logique
 - ∀𝑥 ∀𝑦 𝑞 𝑥, 𝑦 ⇒ 𝑝 𝑥, 𝑦 , ∀𝑧 𝑞(𝑧, 𝑧) ⊨ ∀𝑧 𝑝(𝑧, 𝑧)

Pourquoi?

27
Programmation Logique
 - L’ensemble de formules:
{p(a),
∀𝑥 𝑝 𝑥 ⇒ ¬𝑟 𝑥 ,

∀𝑦 ¬𝑟 𝑦 ⇒ 𝑞 𝑦 ,

∀𝑧 𝑞 𝑧 ⇒ ¬𝑝 𝑧 }
est insatisfiable ou inconsistant

Pourquoi?

28
Programmation Logique
 Calcul des prédicats

II/Mise sous forme clausale d’une

formule

n Forme normale prénexe

n Forme standard de Skolem
n Suppression des ,
n Mise sous-forme FNC
n Séparation
n Renommage

29
Programmation Logique
 Mise sous forme prénexe

30
Programmation Logique
 Calcul des prédicats

Mise sous forme prénexe

n Éliminer les connecteurs  et 

n Transporter les  devant les atomes

l En utilisant les lois de De Morgan

n Transporter les quantificateurs en tête de la formule

l En utilisant les équivalences de formules concernant le
transport des quantificateurs

n Renommer les variables quand cela est nécessaire

l Une variable ne doit pas apparaître en tête de formule 2 fois
quantifiée

31
Programmation Logique
 Calcul des prédicats

Transport des quantificateurs

(x F )  x F xy F  yx F

(x F )  x F xy F  yx F

x F  x H  x(F  H )
x F  x H  x(F  H )
si H ne contient aucune occurrence de x

(x F )  H  x(F  H ) x H  H
(x F )  H  x(F  H ) x H  H

32
Programmation Logique
 33
Programmation Logique
 Calcul des prédicats

Skolemisation

n But: formule sous forme normale prénexe

formule sans quantificateurs existentiels

34
Programmation Logique
 Principe
n y A(y)
Où a est une nouveau symbole
appelé constante de Skolem
A(a)

n x1 x2 … xn y A(x1,x2 … ,xn ,y)

x1 x2 … xn A(x1,x2 … ,xn , f(x1,x2 … ,xn))

Où f est une nouveau symbole appelé fonction de Skolem
35
Programmation Logique
 Exemple:
∃X ∃Y ∀Z ∀T ∃V P(X,Y,Z,T,V)
1. Remplacer X par a (a: nouveau symbole de constante)
∃Y ∀Z ∀T ∃V P(a,Y,Z,T,V)
2. Remplacer Y par b (b: nouveau symbole de constante)
∀Z ∀T ∃V P(a,b,Z,T,V)
3. Remplacer V par f(Z,T) (f: nouveau symbole de fonction)
∀Z ∀T P(a,b,Z,T,f(Z,T))

Lemme : Soit G une formule prénexe et soit G0 une skolémisation

de G. Alors G est satisfiable ssi G0 est satisfiable.

36
Programmation Logique
 Calcul des prédicats

Suppression des 

n forme standard de Skolem

Formule sans 
n Principe sur un exemple:
y z (p(a,y)  q(z,a,y))
Suppression des :
(p(a,y)  q(z,a,y))

37
Programmation Logique
 Mise sous FNC

Exemple:

(¬p(h(x)) ∨ p(y)) ∧ (p(z) ∨ ¬p(h(x))) est une FNC.

38
Programmation Logique
 Séparation:

Exemple:

(¬p(h(x)) ∨ p(y)) ∧ (p(z) ∨ ¬p(h(x)))

Devient l’ensemble de clauses:

{¬p(h(x)) ∨ p(y),
(p(z) ∨ ¬p(h(x))}

39
Programmation Logique
 Renommage:

{¬p(h(x)) ∨ p(y),
(p(z) ∨ ¬p(h(x))}

Devient:

{¬p(h(x)) ∨ p(y),
(p(z) ∨ ¬p(h(x1))}

40
Programmation Logique
 III/ Mise sous forme d’un problème:

n La question à laquelle on s’intéresse est la

suivante: une formule T est-elle conséquence
logique d’un ensemble de formules A?

n Cette question est transformée sous la forme

suivante: A {T} est-elle insatisfiable?
Mise sous forme clausale

S Est-il insatisfiable?

41
Programmation Logique
 42
Programmation Logique
 Exemple

La formule T= x y q(x,y)

est-elle conséquence logique de l’ensemble de

formules A= {x (p(x)   y(r(y)  q(x,y))), x p(x)}
?

43
Programmation Logique
 Exemple (suite)

{x (p(x)   y(r(y)  q(x,y))),

x p(x),
 (x y q(x,y))
}

mise sous forme clausale

S= {p(x)  q(x,f(x)),
p(x)  r(f(x)),
F est-il insatisfiable?
p(a),
q(x,y)
}
44
Programmation Logique
 Mise sous forme clausale de
A={x (p(x)   y(r(y)  q(x,y))),
x p(x),
 (x y q(x,y))
}

45
Programmation Logique
 IV/Méthode de Herbrand

n Principe:

pour savoir si un ensemble de formules possède

un modèle, il suffit de savoir si cet ensemble
possède un modèle « syntaxique »

46
Programmation Logique
 Calcul des prédicats

Univers de Herbrand

n Soit S un ensemble de clauses

l Soit H0 l’ensemble des symboles de constantes ayant
au moins une occurrence dans S. On pose :
Hi = Hi −1   f n (t1,, tn )
pour fn fonction d’arité n de S et tj éléments de Hi-1

l U= limi→ Hi est appelé univers de Herbrand

47
Programmation Logique
 Exemple:

S= {p(x)  q(x,f(x)),
p(x)  r(f(x)),
p(a),
q(x,y)
}

48
Programmation Logique
 n On appelle instance de base d’une clause C
toute clause obtenue en remplaçant les
variables de C par des éléments de H

n Exemples:
l p(a)  q(a,f(a)) est une instance de base de p(x) 
q(x,f(x))
l q(a,a) est une instance de base de q(x,y)
l q(a,f(f(a))) est une instance de base de q(x,y)

49
Programmation Logique
 Calcul des prédicats

Théorème de Herbrand

n Théorème Un ensemble S de clauses est

insatisfiable si et seulement si il existe un
ensemble S’ d’instances de base insatisfiable

n Corollaire Un ensemble de clauses est

satisfiable si et seulement si tout ensemble
fini d’instances de base est satisfiable

50
Programmation Logique
 S= {p(x)  q(x,f(x)),
Exemple(suite)
p(x)  r(f(x)),
p(a),

n Quelques instances de base: q(x,y)

l Fo= p(a)  q(a,f(a)) }
l F1 = p(a)  r(f(a))
l F2 =p(a)
l F3 =q(a,a)
l F4= p(f(a))  q(f(a),f(f(a)))
l F5 = q(a, f(a))
l F6 = q(f(a),a)
l F7 = q(f(a), f(a))
l …..

51
Programmation Logique
 S= {p(x)  q(x,f(x)),
Exemple(suite)
p(x)  r(f(x)),
p(a),

n Quelques instances de base: q(x,y)

l Fo= p(a)  q(a,f(a)) }
l F1 = p(a)  r(f(a))
l F2 =p(a)
l F3 =q(a,a) Instances de base
l F4= p(f(a))  q(f(a),f(f(a))) contradictoires
l F5 = q(a, f(a))
l F6 = q(f(a),a)
l F7 = q(f(a), f(a))
l …..

52
Programmation Logique
 n On a trouvé un ensemble d’instances de base
S’={F0, F2, F5} instatisfiable. Par théorème, S est
insatisfiable.

53
Programmation Logique
 V/ La résolution avec variables (RAV)

n Le théorème de Herbrand ne donne pas un algorithme

efficace.

n La RAV Étend la RSV au cas des formules du calcul des

prédicats

n Fournit une méthode de démonstration automatique

efficace

n Utilise l’unification

54
Programmation Logique
 Notion de substitution

n Une substitution est une fonction permettant de substituer

(=remplacer) des variables d’un terme (ou d’un atome)
par des termes
n Composant d’une substitution: (x/t) où x est une variable
et t est un terme
n Une substitution  = c1 c2 … ck, où ci est un composant
de substitution
n Application d’un composant (x/t) de substitution à un
atome A: (x/t) A= atome obtenu en remplacant toutes les
occurrences de x par t
n Application d’une substitution  = c1 c2 … ck à un atome
A:  A= (c1 (c2 … (ck A)…))
n Substitution identité = 
 A= A

55
Programmation Logique
 Exemple

= (x/f(a)) (y/f(x))
 p(x,y)= (x/f(a)) (y/f(x)) p(x,y)
= ((x/f(a)) ((y/f(x)) p(x,y)))
= ((x/f(a)) p(x,f(x)))
= p(f(a),f(f(a)))

56
Programmation Logique
 Remarque:
attention: l’ordre des composants d’une
substitution est important.
= (y/f(x)) (x/f(a))
 p(x,y)= (y/f(x)) (x/f(a)) p(x,y)
= p(f(a), f(x))

57
Programmation Logique
 Unification

n Unifier deux atomes A et B revient à chercher une

substitution  telle que A= B.
: unificateur de A et B

n  est un plus grand unificateur (pgu) de A et B si pour tout

autre unificateur  de A et B, il existe une substitution 
telle que  =  

n Exemple: Soient A= p(x) et B=p(f(y)). On a  = (x/f(y))

est un unificateur de A et B. Mais on peut trouver d’autres
unificateurs, par exemple,  = (y/a)(x/f(y)) est moins
général que . En effet: si =(y/a) alors  =  

58
Programmation Logique
 Exemples introductifs

n A=p(x,f(a)) B=p(a,z)?

n A=p(x,f(a)) B=p(y,a)?

n A=p(x,f(y)) B=p(a,y)?

59
Programmation Logique
 Algorithme d’unification de deux
atomes A et B

n Input: A, B
n  := 
n Tant que A  B faire
l Déterminer le symbole le plus à gauche de A qui soit différent du
symbole de même rang de B
l Déterminer t1, t2 les sous-termes de A et B qui commencent à ce
symbole
l Si aucun n’est une variable ou l’un est une variable contenue dans
l’autre
Alors echec; arrêt
sinon:
– Déterminer x unevariable parmi t1, t2
– Déterminer t celui de t1, t2 qui n’est pas x
–  :=(x/t) 
finsi
FinTantque
n Output 
60
Programmation Logique
 Remarque:

n L’algorithme précédent calcule le plus grand

unificateur

61
Programmation Logique
 Exemples

n p(x,y) et p(f(a),g(a)) sont unifiables et le plus

grand unificateur est  = (x/f(a)) (z/g(a))
n p(x,y) et r(f(z),y) ne sont pas unifiables
n P(x,y) et p(f(x),y) ne sont pas unifiables

62
Programmation Logique
 Exercice:
Appliquer l’algorithme d’unification pas à pas sur
A=p(a,x,f(g(y))) et B= p(z,f(z),f(u))

63
Programmation Logique
 Exercice:

nDonner un pgu, s’il existe pour:

A= p(x,f(g(x)),a) et B=p(b,y,z)

64
Programmation Logique
 La règle de la résolution

65
Programmation Logique
 Exemple

p(x,c)  r(x) p(c,c)  q(x)

r(c)  q(x)

66
Programmation Logique
 La règle de la diminution permet de réduire le
nombre de littéraux dans une clause

f ⊢𝑑𝑖𝑚 h

Si et seulement si:

l f est de la forme a b  f1
l h est de la forme  a  f1

Où  est un plus grand unificateur de a et b

67
Programmation Logique
 Exemple

p(x,g(y)) p(i(c),z)  r(x,y,z)

68
Programmation Logique
 Le système RAV

n On considère le système formel RAV (Résolution

Avec Variables) tel que:

l Les formules sont des clauses

l Il n’y a pas d’axiomes
l Il y deux règles d’inférence qui sont la résolution et la
diminution

69
Programmation Logique
 Théorème:

Un ensemble de clauses S est insatisafiable si et seulement

si S ⊢ 

70
Programmation Logique
 Exemple S= {p(x)  q(x,f(x)),
p(x)  r(f(x)),
p(a),
q(x,y)}

p(x)  q(x,f(x)) p(a)

q(a,f(a)) q(x,y)

71
Programmation Logique