IA Séance 4

1
La Logique Formelle
Pr. F. BENABBOU FSBM
2020
Master DSBD/S1
Faculté des Sciences Ben M’SIK
Pr. Faouzia Benabbou ([email protected])
Département de mathématiques et Informatique
Faculté des Sciences Ben M’Sik
2
Plan
• Introduction
• Logique formelle et inférence
▫ Représentation des connaissances et inférence LP-LPO
▫ ProLog
• Systèmes experts
• Techniques de représentation et de résolution de problèmes
• Système à base d’agents, Système multi-agents (JADE)
• Introduction à l’apprentissage Automatique
Pr. F. BENABBOU FSBM 2020

3
Langage de la LPO
• Grammaire de la LPO
• L'ensemble des formules bien formées de la logique des prédicats est le plus petit
ensemble de mots construits sur l'alphabet tel que :
terme = constante
| variable
| fonction (terme , ... )
atome = prédicat (terme , ... )
Littéral = terme (positif) |  terme (positif)
formule = littéral
| ∀ variable formule
| ∃ variable formule
| ¬ formule
| formule connecteur formule
connecteur = ∧ | ∨ | ⇒ | ⇔
4
Langage de la LPO
• Exemples de traduction d'énoncés en formules LPO
▫ « Tout est relatif » : ∀x relatif(x)
▫ « Une porte est ouverte ou fermée » : ∀x (porte(x)  (ouvert(x) ∨ fermé(x))
▫ « Une porte est ou bien ouverte ou bien fermée. '' :
∀x ( porte(x)  ((ouvert(x) ∨ fermé(x)) ∧ (ouvert(x) ∧ fermé(x)) )
▫ « Tout ce qui brille n'est pas or » :  ∀x (brille(x)  or(x))
▫ « Il y a des peines, il y a des plaisirs, mais aucune peine n'est un plaisir » :
(∃x peine(x)) ∧ (∃x plaisir(x)) ∧ ∀x (peine(x)  plaisir(x))
▫ « Tous les chemins mènent à Rome » : ∀x (chemin(x)  mène-à(x, Rome))
▫ « Pour tout entier il existe un entier plus grand » :
∀x (entier(x)  ∃y (entier(y) ∧ plus-grand(y , x)) )
▫ « Il existe un plus grand entier » : ∃x (entier(x) ∧ ∀y (entier(y)  plus-grand(x , y)) )
5
Langage de la LPO
• Priorité des connecteurs
▫ Pour éviter les ambiguïtés on fixe une priorité des connecteurs logiques, la voici
en ordre décroissant :
▫ ∀ et ∃ > ¬ > ∨ et ∧ > ⇒ et ⇔.
• Exemple :
▫ ¬r ∨ t ⇒ f signifie ((¬r) ∨ t) ⇒ f
▫ ∀x f(x) ⇒ g(x) signifie (∀x f(x)) ⇒ g(x) qui est différent de ∀x (f(x) ⇒ g(x))

6
Language de la LPO
• Variable libre et liée
▫ Toutes les variables d’une formule sans quantificateurs sont libres.
▫ Une variable est liée ssi elle est dans la portée d’un quantificateur.
▫ Une variable peut être libre et liée à la fois.
• Exemple :
▫ h(x)  m(y) x, y sont libres
▫  x p(x)  m(y , x) x liée, y libre
▫ ( x p(x)q(x))  m(x) x liée et libre
• Fermeture d’une FBF
▫ Une formule où toutes les variables sont liées est dite fermée.
▫ Une formule avec une ou des variables libres est dite ouverte
7
Sémantique de la LPO
• Domaine
▫ Pour évaluer la formule ∀x H(x) il faut connaître l’ensemble des valeurs que
peut prendre la variable x
▫ Cet ensemble est appelé le domaine de discours, noté D
• Interprétation : Une interprétation I d’une formule F est définie par :
▫ le domaine de l’interprétation D non vide
▫ une fonction I qui associe
 à chaque variable une valeur de D
 à chaque constante une valeur de D
 à chaque symbole de fonction à n arguments une fonction de Dn dans D
 à chaque symbole de prédicat à n arguments une application Pn: Dn→{v,f}
8
• Exemple :
soit G=(x) (p(x)  q(f(x),a)) et une interprétation telle que:
I={D={1,2}, a=1, f(1)=2 , f(2)= 1, p(1) →f, p(2) →v, q(1,1) →v, q(1,2) →v, q(2,1) →f,
q(2,2) →f }
pour x=1 p(1)  q(f(1),1)) on a f  f
donc I(G)=v
pour x=2 p(2)  q(f(2),1)) on a v  v
Donc I(G)=v
I est un modèle de G.

9
• Exercice :
▫ Les propositions suivantes sont –elles équivalentes ?
1. (x p(x) ) et  (( x) p(x))
2.  x p(x)  q(x) et ((x p(x))  (x q(x))

10
• Normalisation des formules : Il existe 4 formes d’une formule donnée :
▫ Prénexe
▫ Skolen
▫ Conjonctive
▫ Clausale

11
Forme normale de Prénexe

• Une fbf G est sous forme normale de Prenex ssi G s ’écrit sous la forme:
G=(Q1x1, Q2x2,…..Qnxn) M
où Qi = ou  = Préfixe et M une fbf sans quantificateurs, dite la matrice
• Le but est placer les quantificateurs au début de la formule.
• Théorème : toute formule admet une forme prénexe équivalente

12

• Pour écrire une fbf sous FNP on applique les règles suivantes :
1. Éliminer les quantificateurs redondants (c.-à-d. dont la variable quantifiée
n'est pas employée)
2. Éliminer les doubles implications (ssi)
3. Éliminer les implications simples (si alors)
4. Placer les négations à l'intérieur (par dualité)
5. Renommer les variables quantifiées homonymes
6. Placer les quantificateurs en tête
7. Par distributivité, faire apparaître la forme cherchée.

peut alors être simplifiée en : ∃x (p(x) ∨ q(x)) 13
• Équivalence : Les équivalences de la LP sont conservées, on y ajoute :
• ( x) (M N )  ( x) (N  M), ( x) (M N ) ( x) (N  M)
• ( x) (M  N )  ( x) (N  M), ( x) (M  N ) ( x) (N  M),
• ( x) (N  M)  (x) M  (x) N
• ( x) (N  M)  ( x) M  ( x) N
• (x) M  (x) N  ( x) (M  N) se transforme en (x) M  (y) N
• ( x) (M  N)  ( x) M  ( x) N
• (( x) M (x) ) (( x) N(x))  ( x) ( y) (M (x)  N(y)) renommer les
variables
• (( x) M (x))  (( x) N(x))  ( x) ( y) (M (x)  N(y))
peut alors être simplifiée en : ∃x (p(x) ∨ q(x)) 14
• En plus on a les équivalences suivantes :
( x p(x) )  ( x  p(x))
( x p(x))  ( x p(x) )
• La formule ∀x ∃x (p(x) ∨ q(x)) peut alors être simplifiée en : ∃x (p(x) ∨

q(x))

15
Forme normale de prénexe

• Mise sous forme normale prénexe de la formule :
((∀x) P(x)) ⇒ ((∃x) Q(x) )
1. Suppression de ⇒ : (¬((∀x) P(x))) ∨ (∃x) Q(x)
2. Transfert de la négation (∃x) ¬P(x)) ∨ (∃x) Q(x)
3. Quantificateurs redondants : (∃x) (¬P(x) ∨ Q(x))
• Mise sous forme normale prénexe de la formule : ∀x ∃x (p(x) ∨ q(x))

1. peut alors être simplifiée en : ∃x (P(x) ∨ Q(x))

16
Forme normale de prénexe

• Exemple :
▫ x ([(y p(x))  z q(z, y)]   y r(x, y)) éliminer y
▫ x ( [p(x)  z q(z, y)]    y r(x, y) ) élimination de 
▫ x ( [p(x)  z q(z, y)]   y r(x, y) ) dédoublement y
▫ x ( [p(x)  z q(z, y)]    y1 r(x,y1) ) renommage de y par y1
▫ x ([p(x) z q(z, y)]   y1 r(x,y1) ) morgan
▫ x ([ p(x) z q (z, y)]  y1  r(x, y1)) intériorisation []
▫ x z y1 ([p(x)  q (z, y)]  r(x, y1)) intériorisation
▫ x z y1 [p(x)  r(x, y1)]  [q(z, y) r(x, y1)] quantificateurs

17

• Mise sous forme normale prénexe de la formule :
(∀x p(x) ∧ ∃y q(y)) ⇒ ∃y (p(y) ∧ q(y))
1. Suppression de ⇒ : ¬ (∀x p(x) ∧ ∃y q(y)) ∨ ∃y (p(y) ∧ q(y))
2. Transfert de la négation : (∃x ¬ p(x) ∨ ∀y ¬ q(y)) ∨ ∃y (p(y) ∧ q(y))
3. Renommage des variables : (∃x ¬ p(x) ∨ ∀y ¬ q(y)) ∨ ∃z (p(z) ∧ q(z))
4. Déplacement des quantificateurs : ∃x ∀y ∃z (¬ p(x) ∨ ¬ q(y) ∨ (p(z) ∧ q(z)))
5. Forme normale : ∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y) ∨ p(z)) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(z))

19
Forme normale de Prenex

▫ Exercices : Déterminer une formule prénexe équivalente de :
1. (x P(x)) x (y Q(y) R(x)) )
2. x y R(x,y) x (y R(x,y) R(x,x))
3. x y ((R(x,y) p(x)) z (p(y)g(x,h(z,z))))
4. (x P(x)) x (y Q(y) R(x))
5. (x P(x)) x ((y Q(y)) R(x))
6. (x P(x)) x ( (y Q(y)) R(x))
7. (x P(x)) z ( (y Q(y)) R(z))
8. (x P(x)) z y (Q(y)) R(z))
9. x z y (P(x) (Q(y)) R(z)))
20
Forme standard de Skolen

• Le but est de supprimer les quantificateurs.
• Soit G = (Q1x1)(Q2x2)…..(Qnxn) M une formule sous forme de Prenex
▫ Pour l’écrire sous forme standard de Skolen il faut :
 Mettre G sous FNC M : M=M1  M2  ...  Mq
 Si Qi=  alors :
 s’il n’y a aucun  à gauche de Qi alors supprimer Qixi et remplacer xi par une constante
non déjà existante dans M
 si Q j,..., Ql sont à gauche de Qi et sont tous des  alors supprimer Qixi et remplacer par
une fonction f qui fournit une bonne valeur de xi à partir des valeurs de xj,….,xl.
f : xi → f( xj,….,xl)

21

• Exemple :
▫ xy r(x,y) est ainsi assimilée à x r(x, (x)) où la nouvelle fonction  fournit
symboliquement des  (x) jouant le rôle des y adéquats.
▫ y r(a, y) sera assimilée à r (a, ) où la nouvelle constante a désigné
symboliquement les valeurs pouvant jouer le rôle d'un y adéquat.
▫ x z y1 [p(x)  r(x, y1)]  [q(z, y) r(x, y1)], z et y1 dépendent
respectivement de x plus global, d'où la forme : soient f et g de nouvelles
fonctions telles que f(x) et g(x) symbolisent les instances adéquates de z et y1 :
x [p(x)  r(x, g(x))]  [ q(f(x), y)  r(x, g(x))]

22

1) A = x y  z p(x,y)  q(x,z)
Skolen(A) = x y p(x,y)  q(x,f(x,y))
2) B= x  u y  z( p(x,u)  (q(u,y)  r(y,z)))

Skolen(B) = x y (p(x,f(x))  (q(f(x),y)  r(y,g(x,y))))
3) ∃X ∃Y ∀Z ∀T ∃V P(X,Y,Z,T,V)
1. ∃Y ∀Z ∀T ∃V P(a,Y,Z,T,V)
2. b/Y ∀Z ∀T ∃V P(a,b,Z,T,V)
3. On remplace f(Z,T)/V , ∀Z ∀T P(a,b,Z,T,f(Z,T))
23

• Théorème : si F est une formule, il existe F' forme de Skolem de F et
╞ F ssi ╞ Skolen(F)
• Une fois les quantificateurs existentiels supprimés, toutes les variables
restantes sont quantifiées universellement
• Exemple : ∃x ∀y ∃z ((¬ p(x) ∨ ¬ q(y) ∨ p(z)) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(z))
▫ La variable z est transformée en f(y) :
∃x ∀y ((¬ p(x) ∨ ¬ q(y) ∨ p(f(y))) ∧ (¬ p(x) ∨ ¬ q(y) ∨ q(f(y)))
▫ La variable x est transformée en a constante:
∀y ((¬ p(a) ∨ ¬ q(y) ∨ p(f(y))) ∧ (¬ p(a) ∨ ¬ q(y) ∨ q(f(y)))

24

• Théorème : A est satisfiable ssi skolen(A) l’est.
• Le skolen(A) n’est pas forcément équivalent à A.
• Pour prouver une formule est valide il suffit de monter que sa négation est
inconsistante ou que la forme Skolem de sa négation est inconsistante.
• Exercice :
▫ Mettre sous forme de Skolen
 G1= (x) p(x)  ( y) q(y)
 G2= ( y) q(y)  (x) p(x)
 G3= ∃u ∀x ∃y ∀z ∃t ( p(x) ∧ q(y) ∧ r(x,z,t) ∧ s(y) ∧ k(u) )
25
Forme normale conjonctive / clausale

• Une ou-clause est une formule composée de disjonctions de littéraux
positifs ou négatifs (FND).
▫ p(x,y)  q(x,z,u)   r(t,x)
• Une formule  est sous forme FNC si elle est la conjonction de ou-clause.
▫ (p(x,y)  q(x,z,u)   r(t,x))  ( p(a,y)  t(u))  (d(y))
• Remarque :
▫ Dans une forme clausale on supprime tous les quantificateurs  pour obtenir 
sous forme 1  2 …  n où {1, 2,…, n} est l’ensemble de clauses.
▫  Est la clause vide.

26
Forme normale conjonctive / clausale

• Exercice : Mettre G sous forme de Prenex, sous forme standard de skolen,
puis sous forme normale conjonctive et causale
1) G1 = x y (( E(x,y)  A(x) )   z D(x,z))
2) G2 = ( x) [p(x)  (y) p(y)]
3) G3 = (( x) p(x))  [( y) (y) R]

27
Preuve pour LPO

• On rappelle qu'un système formel est constitué par :
▫ F un ensemble de formules
▫ A un ensemble d'axiomes A  F
▫ un ensemble fini de règles de déduction valides
• Les règles d'inférence utilisées en LP restent valables :
▫ R1: Modus Ponens
▫ R2: Modus tollens
▫ R3: Principe de résolution
• Un exemple d’axiomes du calcul des prédicats (a, b étant des formules et x
une variable)
▫ x a(x) ⇒b(t)
28
Preuve pour LPO

• Schéma axiomatique
▫ Si  est un théorème de la LP et si  est obtenue en substituant dans  une
proposition par une fbf de la LPO alors  est un axiome de la LPO.
• Exemple :
▫ ├ (pq)p est un théorème de la LP
▫ ├ ((x) (p(x) q(x))  (x) p(x), c’ est aussi un axiome de la LPO

29
Validité et consistance
• Exemples :
• x ¬ p(x)  p(x) est une tautologie
• x ¬ p(x)  p(x) est inconsistante
• ( x Personne(x))  ( x (Personne (x)) est valide
• F = {p (a, b),  y p(a, y)} est inconsistante
En effet:  y p(a, y)  y  p(a, y )
F. skolen : F = {p (a, b),  p(a, y )} , Instanciation y = b
F = {p (a, b),  p(a, b )}├ ⃞ par règle de résolution.

30
Principe de résolution en logique des prédicats

• Pour appliquer le principe de résolution à des formes de Skolen, il faut donner des
valeurs aux variables universelles.
• Il est impossible en pratique de résoudre une formule pour toutes les valeurs possibles
des variables sur un domaine.
• En plus, la logique du premier ordre est indécidable, cela signifie qu’il n’existe pas
d’algorithme pour déterminer si une formule est valide ou non valide en un temps fini.
• Néanmoins deux méthodes semi-décidables sont proposées pour essayer d’y remédier :
▫ Jacques Herbrand a introduit une méthode pour démonter qu’une formule F de la LPO est
satisfiable par instanciation, cette méthode consiste à ramener la satisfiabilité d’une
formule en LPO à la LP.
▫ Par unification des termes

31
Théorème de Herbrand
• Le but est de réduire le nombre d’interprétations à prendre en
considération lors d’une procédure de déduction.
• Ainsi étant donnée une formule sous forme de Skolem (sous forme de S),
on peut se limiter pour étudier sa satisfiabilité à son univers de Herbrand.
• Définition : Dans un ensemble de clauses S, un terme de base est un terme
qui ne contient pas de variable, et un atome de base est un atome qui ne
contient pas de variables.
▫ f(x,a) n’est pas un terme de base
▫ P(f(a), f(f(a))) est un atome de base

32
Signature
• Définition : La signature ∑ d’un ensemble S de clause est l’ensemble des
constantes, les fonctions et les prédicats présents dans l’ensemble des
clauses.
▫ S= {P(x)∨ ¬P(f(x)),¬P(a),P(f(f(a)))}, La signature Σ de S comporte une constante
a, un symbole de fonction unaire f et un symbole de relation unaire P.
▫ S= {R(x,s(x)),R(x,y)∧ R(y,z)}
 On Remarque qu’il n’y a pas de constante on en choisit une arbitrairement : a
 La signature Σ de S comporte une constante a, un symbole de fonction unaire s et
un symbole de relation binaire R.

33
Univers de Herbrand
• Définition : L'Univers de Herbrand d'un ensemble de clauses E est
l'ensemble des termes de base que l'on peut construire à partir des
symboles de fonctions et des constantes qui apparaissent dans E.
• L’univers de Herbrand de l'ensemble est stratifié en niveaux.

34
Univers de Herbrand
• Exemple :
1) F= {p(f(x)) ⇒ q(a),r(g(x))}
- La signature Σ de F comporte une constante a, deux symboles de fonction
unaire f et g, et 3 symboles de relation unaire p, q et r.
- L’univers d’herbrand de F est :
Le niveau 0 noté H0 = {a, f(a), g(a)}
Le niveau 1 noté H1 = { a, f(a), g(a), f(f(a)), g(g(a)), f(g(a)) , g(f(a))}
Le niveau ∞ noté H∞ = { a, f(a), g(a), f(f(a)), g(g(a)), f(g(a)) , g(f(a)), f(f(f(a))),
g(f(f(a))), g(g(g(a))), f(g(g(a))), f(f(g(a))), g(f(g(a))) , g(g(f(a))), f(g(f(a))), ……………}

35
• Exemple :
2) H = {P(x), R(x) ∨ Q(y, x), ¬Q(y, y)}
La signature Σ de H comporte une constante a, et 2 symboles de relation unaire P
et R et un symbole de relation binaire Q.
L’univers d’herbrand de H est :
H0 = { a } , H1 = { a } car il n’y a pas de fonction, H∞ = { a }

36
• Exemple :
3) N = {P(f(x) )∨ Q(a), Q(g(b)) ∨ ¬P(y) }
La signature Σ de N comporte 2 constantes a et b, 2 symboles de fonction unaire f
et g et 2 symboles de relation unaire P et Q.
L’univers d’herbrand de N est :
H0 = { a, b, f(a), f(b), g(a), g(b) }
H1 = { a, b, f(a), f(b), g(a), g(b) f(f(a)), f(f(b)), f(g(a)), f(g(b)), g(f(a)), g(f(b)), g(g(a)),
g(g(b)) }
H∞ = H1 ∪ {f(f(f(a))), g(g(g(a))), f(f(f(b))), g(g(g(b))), ……………}

37
Base de Herbrand
• Définition :
La Base de Herbrand d'un ensemble de clauses E est l'ensemble des atomes de
base qui peuvent être construits à partir des symboles de prédicats de E
appliqués aux termes de l'univers de Herbrand de E.

38
Base de Herbrand
• Exemple :
▫ La base de Herbrand de l'ensemble {P(f(x)) ⇒ Q(a),R(g(x))} est :
H ∞ = { a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a)), …}
BH ={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),P(g(a)),Q(g(a)),R(g(a)),...}
▫ La base de Herbrand de l'ensemble S = {P(X), R(X) ∨ Q(Y, X), ¬Q(Y, Y)} :
H ∞ = { a}
BH ={P(a), R(a), Q(a, a)}
▫ La base de Herbrand de l'ensemble S = {P(f(x)) ∨ Q(a), Q(g(b)) ∨ ¬P(y) } :
H ∞ = { a, b, f(a), f(b), g(a), g(b) f(f(a)), f(f(b)), f(g(a)), f(g(b)), g(f(a)), g(f(b)),
g(g(a)), g(g(b)),… }
BH ={P(a), Q(a), P(b), Q(b), P(f(a)), Q(f(a)), P(g(a)), Q(g(a)), ….}
39
Base de Herbrand
• Exemple :
▫ La base de Herbrand de l'ensemble S = {P(f(x)) ∨ Q(a), Q(g(b)) ∨ ¬P(y) } :
H ∞ = { a, b, f(a), f(b), g(a), g(b) f(f(a)), f(f(b)), f(g(a)), f(g(b)), g(f(a)), g(f(b)), g(g(a)),
g(g(b)),… }
BH ={P(a), Q(a), P(b), Q(b), P(f(a)), Q(f(a)), P(g(a)), Q(g(a)), ….}

40
Interprétation de Herbrand
• Définition : soit E un ensemble de clauses, une interprétation de Herbrand
de E est obtenue en remplaçant les variables de E par des éléments de
l'univers de Herbrand de E.
• On note Inst(E) l’ensemble des instances des formules de S obtenues par

substitution des termes de la formule par les termes de l’univers de
Herbrand.

41
Théorème de Herbrand (Herbrand 1929)

• Soit S un ensemble de formules sans quantificateur de signature Σ
▫ ∀(S) a un modèle si et seulement si tout ensemble fini d'instances fermées des
formules de S a un modèle propositionnel
▫ Un ensemble S de clauses est insatisfiable si et seulement s’il existe une
instance S’ Inst(S) fini, sémantiquement inconsistant en logique
propositionnelle.

42
• Soit S= {p(x)  q(y)} D={a,b}
Inst(S)={p(a)  q(a), p(a)  q(b), p(b)  q(a), p(b)  q(b)} est l’ensemble des
instances de S
• S = {P(x),Q(x),¬P(a)∨ ¬Q(b)}
Inst(S)={P(a), Q(a), P(b), Q(b),¬P(a)∨ ¬Q(b)} est l’ensemble des instances de S
• S={¬P(x)  Q(x), P(y) , ¬ Q(a)]
Inst(S)={¬P(a)  Q(a), P(a), ¬ Q(a), ¬P(b)  Q(b), P(b)}

43
• Exemple : Soit S = {P(x)∨Q(x),¬P(a),¬Q(b)}.
▫ H∞ ={a, b}
▫ L’ensemble de toutes les instances sur le domaine de Herbrand est :
Inst(S)={P(a)∨Q(a), P(b)∨Q(b),¬P(a),¬Q(b)}
▫ Soit F1={P(a) Q(a),¬P(a)}  Inst(A) qui est satisfiable dans un modèle où on
I(Q(a))=V
▫ F2={P(a) Q(a),¬P(a), P(b) Q(b),¬Q(b) } qui est satisfiable dans un modèle où
{P(b),Q(a)} ={V , V}
▫ S est satisfiable pour le modèle {P(b),Q(a),P(a),Q(b)} ={V , V, F, F}
▫ Donc l’interprétation de Herbrand associée à S est aussi un modèle de ∀(S).
44
• Exemple :
• Soit S = {P(x),Q(x),¬P(a)∨ ¬Q(b)}
▫ La signature Σ comporte 2 constantes a, b et 2 symboles de relation unaire P, Q.
▫ L’univers d’herbrand de S est {a, b}.
▫ L’ensemble {P(a),Q(a), Q(b),¬P(a)∨ ¬Q(b)} est une instance de S sur le domaine de
Herbrand qui est insatisfiable, donc ∀(S) est insatisfiable.
• Soit S = {P(x),¬P(f(x))}
▫ La signature Σ comporte une constante a, un symbole de fonction unaire f et un
symbole de relation unaire P.
▫ L’univers d’herbrand de S est : {fi(a), i=0,..,n}
▫ L’ensemble {P(a), ¬P(f(a)), P(f(a)),¬P(f(f(a)))} d’instances sur le domaine de Herbrand
est insatisfiable, donc ∀(S) est insatisfiable.
45
• Exemple :
• Soit S = {P(x)∨ ¬P(f(x)),¬P(a),P(f(f(a)))}.
▫ On a la même signature que précédemment.
▫ L’univers d’herbrand de S est : {fi(a), i=0,..,n}
▫ L’ instance {P(a)∨ ¬P(f(a)), ¬P(a), P(f(f(a))), P(f(a))∨ ¬P(f(f(a))) } sur le
domaine de Herbrand est insatisfiable
▫ donc ∀(S) est insatisfiable.
• Dans ce cas il a fallu prendre 2 instances de la première formule de S pour
obtenir une contradiction.

46
Unification et règle de résolution

• Soit ={t1/x1, t2/x2, t3/x3,…, tn/xn} une substitution et  une ebf,  est une
instance de .
• Définition : Une substitution  est dite unificateur pour un ensemble
d’expression {E1, E2,…, En} ssi : E1= E2=...= En..
• On dit que l’ensemble {E1, E2,…, En} est unifiable s’il existe une substitution
 telle que E1= E2=...= En. et  est l’unificateur.
• Exemple :
▫ Soit {P(x, f(y), g(b)), P(x, f(c),g(z)), P(x, f(c),g(u)), P(a, f(y),w)} admet l’unificateur
suivant: ={a/x, c/y, b/z, b/u, g(b)/w}.

47
Unification
• Définition : Un unificateur  pour l’ensemble {E1, E2,…, En} est dit PGU ssi :
  une substitution  telle que :  =  
• Trouver un unificateur le plus général permet d'appliquer le principe de

résolution à des clauses issues de formules du premier ordre.
• L'unificateur le plus général n'existe pas forcément (pas plus qu'un

unificateur) et s'il existe, il n'est pas forcément unique.

48

• Dans la LP, pour établir  de (1 , 2 , 3 ,…, n ), il faut prouver que (1 ,
2 , 3 ,…, n )    ├ ⊥est une contradiction.
• Pour cela il faut :
▫ Il faut mettre (1, 2, 3,…, n ) et   sous FNC et Appliquer le PR en vue
d’obtenir la clause ⊥
• Mais en LPO présence de variable : P(x) Q(x) et  P(f(y))  R (y)

49

• Pour utiliser la réfutation par résolution en calcul des prédicats, il faut
transformer les formules en étapes :
▫ on transforme la formule en FNC (conjonction de clauses)
▫ on transforme les FNC en FNP (prénexe)
▫ on skolémise la formule obtenue pour éliminer les quantificateurs 
▫ Les littéraux et leur négation sont annulés
▫ Trouver la bonne substitution des variables

50

• Exemple : On veut montrer que les trois formules {f1,f2,f3} ├ P(a)
▫ f1 = ∀x ((S(x) ∨ T(x)) ⇒ P(x))
▫ f2 ≡ C3 = ∀x (S(x) ∨ R(x))
▫ f3 ≡ C4= ¬R(a)
▫ Passage en forme clausale : f1 ≡ ∀x ((¬ S(x) ∨ P(x)) ∧ ( (¬ T(x) ∨ P(x)) )
 On a produit donc les deux clauses C1 = ¬S(x) ∨ P(x) C2 = ¬T(x) ∨ P(x)
▫ La négation de la conséquence cherchée donne C5 = ¬P(a).
• Résolution :
1. C1 = ¬S(x) ∨ P(x)
2. C2 = ¬T(x) ∨ P(x)
3. C3 = S(x) ∨ R(x)
4. C4 = ¬R(a)
5. C5 = ¬P(a)
6. C6 = S(a) résolution sur R de C3 et C4 avec x → a
7. C7 = P(a) résolution sur S de C1 et C6 on produit
8. clause vide résolution sur de C5 et C7
• On a donc prouvé la conséquence logique.
51
Propriété de la LPO
• Théorème d'adéquation:
La LPO est correcte : Si ├ A alors ╞ A.
• Théorème de complétude :
La LPO est complète : Si ╞ A alors ├ A
les formules qui sont démontrables formellement, sont exactement les
formules vraies dans tout modèle pour toute interprétation.
▫ si F├P alors F╞P
• La LPO est semi-décidable

52
Décidabilité
• Il existe un algorithme qui, si une formule est démontrable, le dira en un
temps fini, mais qu’on ne peut borner à priori.
• Il n’existe en revanche pas d’algorithme permettant, pour toute formule,
de déterminer en un temps fini qu’elle n’est pas démontrable.

53
LPO et Problèmes SAT

• Problèmes SAT (SATisfiable)
▫ Plusieurs problèmes peuvent être efficacement (en temps polynomial)
réduites à un problème SAT
▫ Le problème de satisfiabilité booléennes de la LP
▫ Premier problème NP-complet
▫ Les Solver SAT ont une très grande importance dans le monde industriel
 Exemple : la conception de circuits intégrés, la planification classique,
l’ordonnancement, la cryptographie, etc.
• Le problème de validité pour les formules booléennes quantifiées
(QSAT) est une généralisation du problème SAT
54

55
Exemple : arbre généalogique en prolog

• homme(albert).
• homme(marc).
• homme(charles).
• femme(sara).
• pere(albert, marc).
• pere(albert, charles).
• pere(albert, sara).
• enfant(X, Y) :- pere(Y, X).
• fils(X, Y) :- enfant(X, Y), homme(X).
• fille(X, Y) :- enfant(X, Y), femme(X).
• frere-ou-soeur(X, Y) :- pere(Z, X), pere(Z, Y), X\=Y.

IA Séance 4

Transféré par

Droits d'auteur :

Formats disponibles

IA Séance 4

Transféré par

Informations du document

Titre original

Copyright

Formats disponibles

Partager ce document

Partager ou intégrer le document

Options de partage

Avez-vous trouvé ce document utile ?

Ce contenu est-il inapproprié ?

Droits d'auteur :

Formats disponibles

IA Séance 4

Transféré par

Droits d'auteur :

Formats disponibles

1

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Forme normale de Prénexe

• Le but est placer les quantificateurs au début de la formule.

• Théorème : toute formule admet une forme prénexe équivalente

Pr. F. BENABBOU FSBM 2020

Forme normale de Prénexe

Pr. F. BENABBOU FSBM 2020

• La formule ∀x ∃x (p(x) ∨ q(x)) peut alors être simplifiée en : ∃x (p(x) ∨

Pr. F. BENABBOU FSBM 2020

Forme normale de prénexe

• Mise sous forme normale prénexe de la formule : ∀x ∃x (p(x) ∨ q(x))

Pr. F. BENABBOU FSBM 2020

Forme normale de prénexe

Pr. F. BENABBOU FSBM 2020

Forme normale de Prénexe

Pr. F. BENABBOU FSBM 2020

Forme normale de Prenex

Forme standard de Skolen

Pr. F. BENABBOU FSBM 2020

Forme standard de Skolen

Pr. F. BENABBOU FSBM 2020

Forme standard de Skolen

2) B= x  u y  z( p(x,u)  (q(u,y)  r(y,z)))

Forme standard de Skolen

Pr. F. BENABBOU FSBM 2020

Forme standard de Skolen

Forme normale conjonctive / clausale

Pr. F. BENABBOU FSBM 2020

Forme normale conjonctive / clausale

Pr. F. BENABBOU FSBM 2020

Preuve pour LPO

Preuve pour LPO

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

• L’univers de Herbrand de l'ensemble est stratifié en niveaux.

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

Principe de résolution en logique des prédicats

Pr. F. BENABBOU FSBM 2020

Principe de résolution en logique des prédicats

• On note Inst(E) l’ensemble des instances des formules de S obtenues par