Intelligence Artificielle AI - Prolog : TD3 avec Correction – Logique
Télécharger PDFBase de l’Intelligence Artificielle : Logique et Formes Normales
Rappels de cours sur les atomes, termes, variables et formules
Un atome (ou formule atomique) est un prédicat directement évaluable à Vrai ou Faux.
Un terme est soit une variable, soit une constante, soit une fonction. Un terme prend sa valeur dans le domaine des variables.
Une variable peut être liée ou libre selon qu’elle est quantifiée (par un quantificateur) ou non.
Une formule est soit un atome, soit une composition de formules avec les connecteurs logiques (¬, ∧, ∨, →, ↔) et les quantificateurs (∀, ∃).
Forme prénexe
Une formule F est prénexe si elle est de la forme Q1x1 Q2x2 ... Qnxn G, où G est sans quantificateur et chaque Qi est soit ∀ soit ∃.
Pour transformer une formule quelconque en forme prénexe, suivez ces étapes :
- Éliminer les connecteurs → et ↔ en appliquant les lois d’équivalence :
- (P → Q) ≡ (¬P ∨ Q)
- (P ↔ Q) ≡ ((P → Q) ∧ (Q → P)))
- Transporter les symboles de négation ¬ devant les formules atomiques (lois de De Morgan, double négation, etc.).
- Renommer les variables si nécessaire pour appliquer les règles d’équivalence lors du déplacement des quantificateurs :
- ∀x (A(x) ∧ B(x)) ≡ ∀x A(x) ∧ ∀x B(x) (mais pas pour ∨ !)
- ∃x (A(x) ∨ B(x)) ≡ ∃x A(x) ∨ ∃x B(x) (mais pas pour ∧ !)
- Transporter les quantificateurs devant la formule pour obtenir une formule prénexe.
Méthode de Skolémisation
La skolémisation permet d’obtenir une forme standard de Skolem à partir d’une formule prénexe F = Q1x1 Q2x2 ... Qnxn G(x1, x2, ..., xn).
Pour skolémiser :
- Éliminer les quantificateurs existentiels Qr :
- Si aucun ∀ n’apparaît avant Qr, remplacez par un nouveau symbole de constante C.
- Si m quantificateurs universels ∀ apparaissent avant Qr, remplacez par une nouvelle fonction de Skolem f d’arité m.
- Itérer le processus jusqu’à ce qu’il n’y ait plus de quantificateurs existentiels dans le préfixe.
Forme clausale de la logique du premier ordre
La forme clausale d’une formule F est obtenue à partir de sa forme standard de Skolem, où :
- Les variables quantifiées universellement sont conservées, et les fonctions (y compris les fonctions de Skolem) ne sont pas modifiées.
- Les variables quantifiées existentiellement sont remplacées par des constantes distinctes.
- Les variables sont renommées d’une clause à l’autre.
Exercice 1 : Formule universellement valide
Considérons la formule F suivante : ∃x ∀y (((U(x) → U(y)) → T(x)) → T(y)).
Pour montrer qu’elle est universellement valide, plusieurs étapes sont nécessaires :
-
Atomes, variables, termes et formules :
- Formules atomiques : U(x), U(y), T(x), T(y).
- Variables : x et y (toutes liées car sous l’emprise d’un quantificateur).
- Termes : x, y.
- Formule à prouver : La négation de la formule à prouver est : ¬(∃x ∀y (((U(x) → U(y)) → T(x)) → T(y))).
- Transformation en forme normale conjonctive : ¬(∃x ∀y (((U(x) → U(y)) → T(x)) → T(y))) ≡ ∀x ∃y ¬(((U(x) → U(y)) → T(x)) → T(y)) ≡ ∀x ∃y ¬(¬((U(x) → U(y)) → T(x)) ∨ T(y)) ≡ ∀x ∃y (¬¬((U(x) → U(y)) → T(x)) ∧ ¬T(y)) ≡ ∀x ∃y ((U(x) → U(y)) → T(x)) ∧ ¬T(y) ≡ ∀x ∃y (¬(¬U(x) ∨ U(y)) ∨ T(x)) ∧ ¬T(y) ≡ ∀x ∃y (U(x) ∧ ¬U(y)) ∨ T(x) ∧ ¬T(y) ≡ ∀x ∃y ((U(x) ∨ T(x)) ∧ (¬U(y) ∨ T(x)) ∧ ¬T(y)).
- Forme prénexe : ∀x ∃y ((U(x) ∨ T(x)) ∧ (¬U(y) ∨ T(x)) ∧ ¬T(y)).
- Skolémisation : ∀x ∃y ((U(x) ∨ T(x)) ∧ (¬U(y) ∨ T(x)) ∧ ¬T(y)) ≡ ∀x (U(x) ∨ T(x)) ∧ (¬U(f(x)) ∨ T(x)) ∧ ¬T(f(x)).
-
Forme clausale :
- C1 = {U(x1) ∨ T(x1)}.
- C2 = {¬U(f(x2)) ∨ T(x2)}.
- C3 = {¬T(f(x3))}.
Résolution avec le principe de réfutation dans le monde de Herbrand
La négation de la formule initiale est insatisfiable, donc la formule initiale est universellement valide.
Exercice 2 : Valider un raisonnement
Pour valider un raisonnement, on établit d’abord ce qui est vrai (conjonction de prédicats) et on nie la conclusion à valider. Si la formule ainsi formée est insatisfiable, la conclusion est correcte.
Exemple :
- Quelques chandelles éclairent très mal : ∃x EM(x).
- Les chandelles sont faites pour éclairer : ∀x FPE(x).
- Donc : quelques objets faits pour éclairer le font très mal : ∃x (FPE(x) ∧ EM(x)).
La négation de la conclusion est insatisfiable en présence des prémisses, donc la conclusion est correcte.
Pour s’entraîner : Mise sous forme prénexe et ses pièges
Exemple 1 :
Formule initiale : (∀x ∃y ∀t R(x, z, y)) → (∃x ∀y ∃t S(x, z, t)).
Transformation en forme prénexe : ∃x ∀y ∃t ¬R(x, z, y) ∨ S(x, z, t).
Exemple 2 :
Formule initiale : (∀x ∃y ∀t R(x, z, t)) → (∃x ∀y ∃t S(x, z, t)).
Transformation en forme prénexe : ∃x ∃t ¬R(x, z, t) ∨ S(x, z, t).
FAQ
1. Qu’est-ce qu’un quantificateur universel (∀) et un quantificateur existentiel (∃) ?
Un quantificateur universel ∀x signifie "pour tout x", tandis qu’un quantificateur existentiel ∃x signifie "il existe un x". Ils lient les variables et déterminent leur portée dans une formule.
2. Pourquoi est-il nécessaire de transformer une formule en forme prénexe avant la skolémisation ?
La forme prénexe standardise la position des quantificateurs, ce qui facilite l’application des règles de skolémisation et simplifie la transformation en forme clausale.
3. Que signifie une clause vide dans le cadre de la réfutation ?
Une clause vide signifie que la formule est insatisfiable, donc sa négation est toujours vraie. Dans le principe de réfutation, cela prouve que la conclusion est correcte.