Séance 2 — L’IA qui raisonne
Logique, inférence, résolution, unification
Amont. L’agent fondé sur un modèle de la Séance 1, qui tient un état interne parce que l’environnement est partiellement observable, et la description PEAS d’une tâche.
Aval. La logique dit où sont les dangers, pas quelle suite d’actions mène au but : c’est l’objet de la recherche (Séance 3). Elle ne connaît que le vrai et le faux : la Séance 5 reprendra le Monde de Bouki avec un odorat imparfait et des croyances graduées, la Séance 6 y prendra des décisions.
- Écrire des formules de logique propositionnelle, les évaluer dans une interprétation, reconnaître un modèle.
- Distinguer formule satisfiable, valide, insatisfiable ; décider \(\mathrm{KB}\models\alpha\) par vérification de modèles.
- Mettre une formule en forme normale conjonctive ; reconnaître une clause de Horn.
- Distinguer la dérivabilité \(\vdash\) de la conséquence logique \(\models\) ; dérouler un chaînage avant et un chaînage arrière.
- Conduire une preuve par réfutation jusqu’à la clause vide, et en connaître la correction et la complétude.
- Formaliser en logique du premier ordre, mettre en forme clausale (skolémisation), unifier deux termes (unificateur le plus général, test d’occurrence), résoudre au premier ordre.
- Situer les systèmes experts et le calcul symbolique ; utiliser SymPy pour vérifier un raisonnement.
L’agent fondé sur les connaissances
Le raisonnement au-delà du réflexe
La Séance 1 a construit des agents de plus en plus riches. L’agent réflexe réagit au percept courant ; l’agent fondé sur un modèle garde un état interne, mis à jour par une formule (l’humidité du sol, qui baisse de 6 points par heure). Cette séance franchit un pas de plus : un agent qui raisonne combine ce qu’il a perçu à des règles générales, pour en tirer des connaissances qu’aucun capteur ne lui donne.
L’exemple qui sert de fil rouge le montre. Ousmane explore une grotte en grille. Il sent une odeur dans la case \((2,1)\) : la hyène Bouki est dans une case voisine. Un agent réflexe muni de la règle « si odeur, alors fuir » reculerait ; or Bouki peut se trouver en \((2,2)\) comme en \((3,1)\), et seule la combinaison avec ce qu’Ousmane a perçu ailleurs permet de trancher. La question de la séance est donc double : comment un agent représente-t-il ce qu’il sait, et comment en tire-t-il, de façon correcte, tout ce qui en découle ? La réponse de l’IA symbolique tient en deux mots : un langage formel, la logique, et des règles d’inférence qui ne produisent que des conséquences de ce qui est su.
Base de connaissances, TELL et ASK
Un agent fondé sur les connaissances dispose d’une base de connaissances (KB), un ensemble de formules d’un langage logique, et de deux opérations : TELL ajoute une formule à la base (un percept, une règle) ; ASK demande au moteur d’inférence ce qui découle de la base. À chaque pas, l’agent perçoit, informe sa base (TELL), l’interroge (ASK) et agit.
C’est une réalisation de l’agent fondé sur un modèle de la Séance 1 : le modèle du monde est la base de connaissances, sa mise à jour est TELL, le choix de l’action passe par ASK. Sa force tient à la séparation entre les connaissances et le moteur : le moteur d’inférence ne dépend pas du domaine, et changer de domaine revient à changer les formules de la base. C’est l’approche déclarative : on dit à l’agent ce qui est vrai, pas comment agir dans chaque cas.
Le fil rouge : le Monde de Bouki
Ousmane explore une grotte de Kédougou, représentée par une grille \(4\times4\), à la recherche d’or. Bouki, la hyène des contes wolof, occupe une case, un puits une autre ; entrer dans l’une de ces cases est mortel. Ousmane part de \((1,1)\), case sûre. La case \((i,j)\) est à la ligne \(i\) (comptée du bas) et à la colonne \(j\). Dans la case où il se trouve, Ousmane perçoit une odeur si Bouki est dans une case voisine (nord, sud, est ou ouest, pas en diagonale), une brise si un puits est voisin, et un éclat sur la case de l’or.
La figure montre la grotte entière, telle qu’Ousmane ne la voit jamais : Bouki en \((2,2)\), le puits en \((3,3)\), l’or en \((4,4)\), et les percepts qu’ils provoquent. La description PEAS et les propriétés de l’environnement (Séance 1) sont les suivantes.
| P | \(+1000\) pour l’or, \(-1000\) pour la mort, \(-1\) par déplacement | partiellement observable | percepts locaux seulement |
|---|---|---|---|
| E | grille \(4\times4\), Bouki, un puits, l’or | déterministe | un déplacement réussit toujours |
| A | aller au nord, au sud, à l’est, à l’ouest, ramasser l’or | séquentiel | chaque pas engage la suite |
| S | odeur, brise, éclat dans la case courante | statique, discret, mono-agent | Bouki et le puits restent en place |
L’observabilité partielle rend le raisonnement indispensable : l’agent doit combler l’écart entre ce qu’il perçoit et ce qu’il doit savoir pour ne pas mourir. Le déterminisme et la statique rendent la logique adaptée : un fait établi le reste, et une règle du monde ne souffre pas d’exception.
Repères historiques
Le projet de réduire le raisonnement à un calcul est ancien. Boole publie en 1854 The Laws of Thought, un calcul algébrique des propositions ; Frege introduit en 1879, dans la Begriffsschrift, les quantificateurs de la logique du premier ordre. L’IA reprend ce projet dès sa fondation : en 1956, le Logic Theorist de Newell, Shaw et Simon démontre des théorèmes des Principia Mathematica. En 1960, Davis et Putnam proposent un algorithme de satisfiabilité, amélioré en 1962 par Davis, Logemann et Loveland (DPLL), ancêtre des solveurs SAT actuels. En 1965, Robinson publie dans le Journal of the ACM le principe de résolution et l’unification, une règle unique pour toute la logique du premier ordre. En 1971, Cook démontre que le problème SAT est NP-complet. En 1972, Colmerauer et Roussel créent à Marseille le langage Prolog, qui exécute des programmes écrits en clauses de Horn par résolution. Les années 1970 voient enfin les systèmes experts, dont MYCIN, développé à Stanford par Edward Shortliffe, est le plus connu (section Section 9).
La logique propositionnelle : syntaxe
Propositions atomiques et connecteurs
Une proposition atomique, ou symbole propositionnel, est un énoncé qui prend la valeur vrai (V) ou faux (F), et une seule. Choisir les symboles est un acte de modélisation : c’est décider ce que l’agent représente du monde.
Pour la grotte, Ousmane utilise quatre familles de symboles : \(B_{i,j}\) (Bouki est en \((i,j)\)), \(P_{i,j}\) (un puits est en \((i,j)\)), \(O_{i,j}\) (une odeur est perçue en \((i,j)\)), \(\mathit{Br}_{i,j}\) (une brise est perçue en \((i,j)\)). Avec 16 cases, cela fait 64 symboles. Les symboles se combinent par des connecteurs.
| connecteur | nom | lecture | exemple |
|---|---|---|---|
| \(\neg\) | négation | non | \(\neg B_{1,2}\) : Bouki n’est pas en \((1,2)\) |
| \(\land\) | conjonction | et | \(O_{2,1}\land\neg\mathit{Br}_{2,1}\) |
| \(\lor\) | disjonction | ou (inclusif) | \(B_{2,2}\lor B_{3,1}\) |
| \(\to\) | implication | si… alors | \(\neg O_{1,1}\to\neg B_{1,2}\) |
| \(\leftrightarrow\) | équivalence | si et seulement si | \(O_{1,1}\leftrightarrow(B_{1,2}\lor B_{2,1})\) |
La dernière formule est une règle du monde : il y a une odeur en \((1,1)\) si et seulement si Bouki est dans l’une des deux cases voisines. Les règles du monde sont connues d’avance ; les percepts s’ajoutent au fil de l’exploration.
Formules bien formées et priorités
- Un symbole est une formule ; (2) si \(\varphi\) est une formule, \(\neg\varphi\) en est une ; (3) si \(\varphi\) et \(\psi\) sont des formules, \((\varphi\land\psi)\), \((\varphi\lor\psi)\), \((\varphi\to\psi)\) et \((\varphi\leftrightarrow\psi)\) en sont ; (4) rien d’autre n’est une formule.
La définition est récursive : un programme reconnaît une formule et l’évalue en suivant la même récursion. Pour alléger l’écriture, les connecteurs ont une priorité décroissante : \(\neg\), puis \(\land\), puis \(\lor\), puis \(\to\), puis \(\leftrightarrow\). Ainsi \(\neg P\land Q\to R\) se lit \(((\neg P)\land Q)\to R\).
\(P\to Q\) n’est fausse que si \(P\) est vraie et \(Q\) fausse. Quand \(P\) est fausse, \(P\to Q\) est vraie, quelle que soit \(Q\) : « si Dakar est en Europe, alors Touba est sur la Lune » est une formule vraie. L’implication logique n’exprime aucun lien de cause ; elle exprime une promesse, qui n’est rompue que si la condition est remplie sans que la conclusion le soit.
La logique propositionnelle : sémantique
Tables de vérité
La sémantique donne un sens aux formules : elle dit quand une formule est vraie. Chaque connecteur est défini par sa table de vérité. Le programme suivant l’écrit pour les cinq connecteurs, dans l’ordre \(P\), \(Q\), \(\neg P\), \(P\land Q\), \(P\lor Q\), \(P\to Q\), \(P\leftrightarrow Q\) ; l’implication s’écrit \((\neg p)\lor q\), l’équivalence est l’égalité des valeurs.
from itertools import product
def implique(p, q):
return (not p) or q
for p, q in product([True, False], repeat=2):
print(p, q, not p, p and q, p or q, implique(p, q), p == q)La sortie est :
True True False True True True True
True False False False True False False
False True True False True True False
False False True False False True TrueL’avant-dernière colonne n’a qu’un F, à la deuxième ligne : \(P\) vraie, \(Q\) fausse.
Interprétation et modèle
Une interprétation \(m\) attribue une valeur de vérité à chaque symbole ; avec \(n\) symboles, il y a \(2^n\) interprétations. La valeur d’une formule dans \(m\) se calcule par les tables de vérité, de l’intérieur vers l’extérieur. \(m\) est un modèle de \(\varphi\) si \(\varphi\) est vraie dans \(m\) ; on note \(m\models\varphi\), et \(\mathrm{Mod}(\varphi)\) l’ensemble des modèles de \(\varphi\). Un modèle d’une base est un modèle de toutes ses formules.
Une interprétation est un monde possible. L’agent ne sait pas dans quel monde il se trouve, mais chaque percept écarte des mondes : ceux où le percept serait faux. Le programme évalue la règle de l’odeur en \((2,1)\) dans deux interprétations.
def regle21(m):
# O21 <-> (B11 ou B22 ou B31) : odeur en (2,1) ssi Bouki voisin
return m["O21"] == (m["B11"] or m["B22"] or m["B31"])
ma = {"O21": True, "B11": False, "B22": True, "B31": False}
mb = {"O21": True, "B11": False, "B22": False, "B31": False}
print(regle21(ma), regle21(mb))
print(2 ** len(ma))La sortie est :
True False
16Dans ma, il y a une odeur et Bouki est en \((2,2)\) : la règle est vraie, ma en est un modèle. Dans mb, il y a une odeur mais aucun Bouki voisin : la règle est fausse. Quatre symboles donnent 16 interprétations.
Satisfiable, valide, insatisfiable
Une formule est satisfiable si elle a au moins un modèle, valide (une tautologie) si toute interprétation en est un modèle, insatisfiable (une contradiction) si elle n’en a aucun.
\(P\land Q\) est satisfiable sans être valide ; \(P\lor\neg P\) est valide (le tiers exclu) ; \(P\land\neg P\) est insatisfiable. Les trois notions sont liées par la négation : \(\varphi\) est valide si et seulement si \(\neg\varphi\) est insatisfiable. Ce lien, qui paraît anodin, fonde la preuve par réfutation de la section Section 6.
La conséquence logique
Une formule \(\alpha\) est conséquence logique d’une base KB, noté \(\mathrm{KB}\models\alpha\), si tout modèle de KB est un modèle de \(\alpha\) : \(\mathrm{Mod}(\mathrm{KB})\subseteq\mathrm{Mod}(\alpha)\). De manière équivalente, \(\mathrm{KB}\models\alpha\) si et seulement si \(\mathrm{KB}\land\neg\alpha\) est insatisfiable.
La seconde forme découle de la première : \(\mathrm{KB}\land\neg\alpha\) a un modèle exactement quand un modèle de KB rend \(\alpha\) fausse. Par exemple \(\{P,\ P\to Q\}\models Q\) : le seul modèle des deux prémisses est \(P=Q=\) V, qui rend \(Q\) vraie. Plus la base contient de formules, moins elle a de modèles, et plus elle a de conséquences ; c’est pourquoi chaque percept enrichit ce que l’agent sait.
Le raisonnement d’Ousmane en trois cases
Ousmane part de \((1,1)\), va en \((2,1)\), revient, puis va en \((1,2)\). La figure résume ce qu’il sait après chaque case.
En \((1,1)\), ni odeur ni brise. Avec la règle \(O_{1,1}\leftrightarrow(B_{1,2}\lor B_{2,1})\), l’absence d’odeur donne \(\neg B_{1,2}\land\neg B_{2,1}\) ; la règle de la brise donne de même \(\neg P_{1,2}\land\neg P_{2,1}\) : les deux voisines sont sûres. En \((2,1)\), une odeur, pas de brise : la règle \(O_{2,1}\leftrightarrow(B_{1,1}\lor B_{2,2}\lor B_{3,1})\), avec \(\neg B_{1,1}\) (le départ est sûr), donne \(B_{2,2}\lor B_{3,1}\) ; l’absence de brise écarte les puits en \((2,2)\) et en \((3,1)\). À ce stade, deux mondes restent possibles pour Bouki. En \((1,2)\), une odeur encore : \(B_{1,3}\lor B_{2,2}\). Bouki n’occupe qu’une case : s’il était en \((3,1)\), la seconde disjonction exigerait un second Bouki en \((1,3)\). Il reste \(B_{2,2}\), et les cases \((3,1)\) et \((1,3)\) sont sûres.
Sans la règle « un seul Bouki », \(B_{2,2}\) n’est pas une conséquence : un monde avec deux Bouki, en \((1,3)\) et en \((3,1)\), rend vrais tous les percepts. Une conclusion logique n’est jamais plus sûre que les règles du monde qu’elle utilise ; l’unicité doit être écrite dans la base, par exemple par les clauses \(\neg B_{1,3}\lor\neg B_{2,2}\), \(\neg B_{1,3}\lor\neg B_{3,1}\), \(\neg B_{2,2}\lor\neg B_{3,1}\).
Exemple pas à pas : la vérification de modèles
La définition de \(\models\) donne directement un algorithme : énumérer toutes les interprétations, garder les modèles de la base, vérifier que \(\alpha\) est vraie dans chacun. Après élimination des cases déjà écartées, trois symboles décrivent les positions encore possibles de Bouki : \(B_{1,3}\), \(B_{2,2}\), \(B_{3,1}\). La base en contient l’essentiel : \(r_1=B_{2,2}\lor B_{3,1}\) (odeur en \((2,1)\)), \(r_2=B_{1,3}\lor B_{2,2}\) (odeur en \((1,2)\)), et l’unicité, écrite « au plus un symbole vrai ».
SYMB = ["B13", "B22", "B31"]
def kb(m):
r1 = m["B22"] or m["B31"] # odeur (2,1)
r2 = m["B13"] or m["B22"] # odeur (1,2)
un = sum(m.values()) <= 1 # un seul Bouki
return r1 and r2 and un
def consequence(kb, alpha):
ok = True
for vals in product([False, True], repeat=3):
m = dict(zip(SYMB, vals))
if kb(m):
print(vals, alpha(m))
ok = ok and alpha(m)
return ok
print(consequence(kb, lambda m: m["B22"]))La fonction consequence parcourt les huit interprétations dans l’ordre de product (F avant V), construit le dictionnaire m (ligne 10), évalue la base (lignes 3 à 6, appelées par la ligne 11) et, si la base est vraie, affiche l’interprétation et la valeur de \(\alpha\) (ligne 12) puis l’intègre au verdict (ligne 13). La table donne les huit tours.
| Tour | Lignes | \(B_{1,3}\) | \(B_{2,2}\) | \(B_{3,1}\) | \(r_1\) | \(r_2\) | un | KB | \(\alpha\) |
|---|---|---|---|---|---|---|---|---|---|
| 1 | 3–6, 10–11 | F | F | F | F | F | V | F | — |
| 2 | 3–6, 10–11 | F | F | V | V | F | V | F | — |
| 3 | 3–6, 10–13, 15 | F | V | F | V | V | V | V | V |
| 4 | 3–6, 10–11 | F | V | V | V | V | F | F | — |
| 5 | 3–6, 10–11 | V | F | F | F | V | V | F | — |
| 6 | 3–6, 10–11 | V | F | V | V | V | F | F | — |
| 7 | 3–6, 10–11 | V | V | F | V | V | F | F | — |
| 8 | 3–6, 10–11 | V | V | V | V | V | F | F | — |
Aux tours 1 et 2, \(r_1\) ou \(r_2\) est fausse : aucun Bouki ne rend compte des deux odeurs. Au tour 3, \((B_{1,3},B_{2,2},B_{3,1})=(\mathrm{F},\mathrm{V},\mathrm{F})\) rend tout vrai : c’est un modèle de la base, et \(\alpha=B_{2,2}\) y est vraie ; la ligne 12 l’affiche. Aux tours 4 à 8, chaque interprétation contient au moins deux Bouki, ou rend fausse l’une des odeurs : le tour 6, \((\mathrm{V},\mathrm{F},\mathrm{V})\), satisfait \(r_1\) et \(r_2\) mais viole l’unicité. La base a un seul modèle ; \(\alpha\) y est vraie, donc \(\mathrm{KB}\models B_{2,2}\). Les figures montrent l’état au tour 3 et l’état final.
La sortie est :
(False, True, False) True
TrueLa méthode est correcte et complète, et elle termine toujours en logique propositionnelle ; mais elle examine \(2^n\) interprétations. Chaque symbole de plus double le travail :
for n in [3, 16, 32, 64]:
print(n, f"{2 ** n:.3g}")La sortie est :
3 8
16 6.55e+04
32 4.29e+09
64 1.84e+19Les 64 symboles de la grotte donnent \(1{,}84\times10^{19}\) interprétations. Il faut des méthodes qui manipulent les formules au lieu d’énumérer les mondes : les règles d’inférence et la résolution.
Équivalences et formes normales
Équivalence logique
Deux formules sont logiquement équivalentes, \(\varphi\equiv\psi\), si elles ont les mêmes modèles. Remplacer une formule par une formule équivalente ne change rien à ce que l’agent sait ; les équivalences suivantes servent de règles de réécriture.
| élimination de \(\to\) | \(P\to Q\equiv\neg P\lor Q\) |
|---|---|
| élimination de \(\leftrightarrow\) | \(P\leftrightarrow Q\equiv(P\to Q)\land(Q\to P)\) |
| lois de De Morgan | \(\neg(P\land Q)\equiv\neg P\lor\neg Q\), \(\neg(P\lor Q)\equiv\neg P\land\neg Q\) |
| double négation | \(\neg\neg P\equiv P\) |
| contraposition | \(P\to Q\equiv\neg Q\to\neg P\) |
| distributivité | \(P\lor(Q\land R)\equiv(P\lor Q)\land(P\lor R)\), \(P\land(Q\lor R)\equiv(P\land Q)\lor(P\land R)\) |
| idempotence, absorption | \(P\lor P\equiv P\), \(P\land(P\lor Q)\equiv P\), \(P\lor(P\land Q)\equiv P\) |
Par exemple, \(\neg(P\to Q)\equiv\neg(\neg P\lor Q)\equiv\neg\neg P\land\neg Q\equiv P\land\neg Q\) : dire qu’une implication est fausse, c’est dire que la prémisse est vraie et la conclusion fausse, ce que montrait la table de vérité.
La forme normale conjonctive
Les algorithmes d’inférence travaillent sur une forme standard des formules.
Un littéral est un symbole ou sa négation. Une clause est une disjonction de littéraux ; la clause vide, notée \(\square\), n’a aucun littéral et est fausse dans toute interprétation. Une formule est en forme normale conjonctive (FNC) si elle est une conjonction de clauses.
- Éliminer \(\leftrightarrow\) : \(\varphi\leftrightarrow\psi\) devient \((\varphi\to\psi)\land(\psi\to\varphi)\).
- Éliminer \(\to\) : \(\varphi\to\psi\) devient \(\neg\varphi\lor\psi\).
- Porter les négations sur les symboles (De Morgan, double négation).
- Distribuer \(\lor\) sur \(\land\), jusqu’à obtenir une conjonction de disjonctions de littéraux.
Chaque étape remplace une formule par une formule équivalente : toute formule a une FNC équivalente. Appliquée à la règle de l’odeur en \((2,1)\), la recette donne, étape 1 : \[(O_{2,1}\to B_{1,1}\lor B_{2,2}\lor B_{3,1})\land(B_{1,1}\lor B_{2,2}\lor B_{3,1}\to O_{2,1})~;\] étape 2 : \((\neg O_{2,1}\lor B_{1,1}\lor B_{2,2}\lor B_{3,1})\land(\neg(B_{1,1}\lor B_{2,2}\lor B_{3,1})\lor O_{2,1})\) ; étape 3 : la négation de la disjonction devient \(\neg B_{1,1}\land\neg B_{2,2}\land\neg B_{3,1}\) ; étape 4 : la distribution de \(\lor O_{2,1}\) sur cette conjonction donne trois clauses. Au total : \[(\neg O_{2,1}\lor B_{1,1}\lor B_{2,2}\lor B_{3,1})\land(\neg B_{1,1}\lor O_{2,1})\land(\neg B_{2,2}\lor O_{2,1})\land(\neg B_{3,1}\lor O_{2,1}).\] La première clause dit « odeur, donc un Bouki voisin » ; les trois autres, « un Bouki voisin, donc odeur ». SymPy trouve la même FNC :
from sympy import symbols, Or, And, Not, Equivalent, to_cnf
O21, B11, B22, B31 = symbols("O21 B11 B22 B31")
regle = Equivalent(O21, Or(B11, B22, B31))
print(to_cnf(regle))La sortie est :
(O21 | ~B11) & (O21 | ~B22) & (O21 | ~B31) & (B11 | B22 | B31 | ~O21)La distribution peut faire croître la formule de façon exponentielle : \((P_1\land Q_1)\lor(P_2\land Q_2)\lor\cdots\lor(P_n\land Q_n)\) a une FNC de \(2^n\) clauses, une par choix d’un littéral dans chaque conjonction. La transformation de Tseitin évite cette explosion en introduisant des symboles auxiliaires ; la formule obtenue n’est plus équivalente à l’originale, mais elle est équisatisfiable : satisfiable si et seulement si l’originale l’est, ce que demande la réfutation.
Forme normale disjonctive et clauses de Horn
Une formule est en forme normale disjonctive (FND) si elle est une disjonction de conjonctions de littéraux.
La FND est le dual de la FNC. Une FND est satisfiable si et seulement si l’une de ses conjonctions ne contient pas à la fois un littéral et sa négation : chaque conjonction décrit une famille de modèles. Ce test est rapide, mais la construction d’une FND est en général exponentielle ; c’est la FNC qui sert à l’inférence.
Une clause de Horn a au plus un littéral positif. Une clause définie en a exactement un : \(\neg P_1\lor\cdots\lor\neg P_k\lor Q\equiv(P_1\land\cdots\land P_k)\to Q\) ; si \(k=0\), c’est un fait, \(Q\). Une clause but n’a aucun littéral positif : \(\neg P_1\lor\cdots\lor\neg P_k\), soit \((P_1\land\cdots\land P_k)\to\bot\).
Une clause définie est une règle « si conditions, alors conclusion », la forme naturelle d’une connaissance d’expert ou d’un programme Prolog. Sur une base de clauses définies, décider si un symbole est conséquence de la base se fait en temps linéaire en la taille de la base, par les chaînages de la section suivante. La clause \(\neg O_{2,1}\lor B_{1,1}\lor B_{2,2}\lor B_{3,1}\), avec trois littéraux positifs, n’est pas une clause de Horn.
L’inférence et les chaînages
Dérivabilité et conséquence logique
La vérification de modèles parle des mondes ; une règle d’inférence parle des formules. Le lien entre ces deux points de vue est le cœur de la logique.
\(\mathrm{KB}\vdash_i\alpha\) signifie que \(\alpha\) est dérivable de KB par les règles de la procédure d’inférence \(i\) : une suite d’opérations sur les symboles, sans référence aux modèles. La procédure \(i\) est correcte si \(\mathrm{KB}\vdash_i\alpha\) entraîne \(\mathrm{KB}\models\alpha\) : elle ne dérive que des conséquences. Elle est complète si \(\mathrm{KB}\models\alpha\) entraîne \(\mathrm{KB}\vdash_i\alpha\) : elle dérive toutes les conséquences.
Une procédure correcte peut être incomplète : elle se tait sur des conséquences qu’elle ne sait pas atteindre. Une procédure incorrecte est inutilisable : elle peut dériver \(\alpha\) dans une base où \(\alpha\) est fausse dans certains modèles.
Règles d’inférence
Une règle d’inférence s’écrit \(\frac{\text{prémisses}}{\text{conclusion}}\) ; elle est correcte si tout modèle des prémisses est un modèle de la conclusion.
| modus ponens | \(\dfrac{P\to Q P}{Q}\) | modus tollens | \(\dfrac{P\to Q \neg Q}{\neg P}\) |
|---|---|---|---|
| élimination du \(\land\) | \(\dfrac{P\land Q}{P}\) | syllogisme hypothétique | \(\dfrac{P\to Q Q\to R}{P\to R}\) |
« Si Amadou rate le bus Dakar Dem Dikk de 7 h, il arrive en retard au travail ; il l’a raté ce matin » : il arrive en retard (modus ponens). « Si le thiéboudienne est bien cuit, le riz est tendre ; le riz n’est pas tendre » : il n’est pas bien cuit (modus tollens, qui raisonne de la conclusion fausse vers la prémisse). Ces règles sont correctes, mais aucune combinaison d’entre elles n’est complète : la base \(\{P\lor Q,\ P\to R,\ Q\to R\}\) a pour conséquence \(R\) (si \(P\) est vraie, \(R\) l’est ; si \(Q\) est vraie, aussi), et le modus ponens seul ne la dérive pas, faute de connaître \(P\) ou \(Q\). Il manque la preuve par cas ; la résolution de la section Section 6 la contient.
Une base de Horn pour le Monde de Bouki
Les règles du monde sont des équivalences ; leur conséquence la plus utile pour l’action, « telle case est sûre », s’écrit en clauses définies, à la manière d’un système expert qui aurait compilé ces règles. Les symboles sont : R11, ni odeur ni brise en \((1,1)\) ; O21 et O12, une odeur en \((2,1)\) et en \((1,2)\) ; C21 et C12, pas de brise (calme) en \((2,1)\) et en \((1,2)\) ; B22, Bouki en \((2,2)\) ; OK\(_{i,j}\), ni Bouki ni puits en \((i,j)\).
REGLES = [(["R11"], "OK12"), (["R11"], "OK21"),
(["O21", "O12"], "B22"),
(["B22", "C21"], "OK31"), (["B22", "C12"], "OK13")]
FAITS = ["R11", "O21", "C21", "O12", "C12"]
print(len(REGLES), len(FAITS))La sortie est :
5 5Chaque règle est une conséquence logique des règles du monde (odeur, brise, unicité de Bouki) : « \((1,1)\) calme, donc \((1,2)\) et \((2,1)\) sûres », « deux odeurs, donc Bouki en \((2,2)\) », « Bouki en \((2,2)\) et pas de brise en \((2,1)\), donc \((3,1)\) sûre », et de même pour \((1,3)\). La question posée est OK13 : la case \((1,3)\) est-elle sûre ?
Exemple pas à pas : le chaînage avant
Le chaînage avant part des faits et applique les règles dont toutes les prémisses sont connues, en ajoutant leurs conclusions aux faits, jusqu’à atteindre le but ou ne plus rien produire. Il est dirigé par les données.
L’implémentation tient un agenda, la file des symboles établis mais pas encore traités, et un compteur par règle, le nombre de ses prémisses non encore établies.
def chainage_avant(regles, faits, q):
compte = [len(pr) for pr, c in regles]
infere = set()
agenda = list(faits)
while agenda:
p = agenda.pop(0)
if p == q:
return True
if p not in infere:
infere.add(p)
print(p, end=" ")
for i, (pr, c) in enumerate(regles):
if p in pr:
compte[i] -= 1
if compte[i] == 0:
agenda.append(c)
return False
print(chainage_avant(REGLES, FAITS, "OK13"))Au départ (lignes 2 à 4), les compteurs valent 1, 1, 2, 2, 2 et l’agenda contient les cinq faits. À chaque tour, la ligne 6 retire la tête de l’agenda ; si c’est le but, la ligne 8 rend True. Sinon, un symbole nouveau est marqué inféré (ligne 10), affiché (ligne 11), et chaque règle qui l’a en prémisse perd une unité (ligne 14) ; une règle dont le compteur tombe à 0 a toutes ses prémisses établies, et sa conclusion entre dans l’agenda (ligne 16).
| Tour | Lignes | sort | compteurs modifiés | ajouté | agenda après le tour |
|---|---|---|---|---|---|
| 1 | 6–7, 9–16 | R11 | \(c_{1}=0\), \(c_{2}=0\) | OK12, OK21 | O21 C21 O12 C12 OK12 OK21 |
| 2 | 6–7, 9–15 | O21 | \(c_{3}=1\) | — | C21 O12 C12 OK12 OK21 |
| 3 | 6–7, 9–15 | C21 | \(c_{4}=1\) | — | O12 C12 OK12 OK21 |
| 4 | 6–7, 9–16 | O12 | \(c_{3}=0\) | B22 | C12 OK12 OK21 B22 |
| 5 | 6–7, 9–15 | C12 | \(c_{5}=1\) | — | OK12 OK21 B22 |
| 6 | 6–7, 9–13 | OK12 | — | — | OK21 B22 |
| 7 | 6–7, 9–13 | OK21 | — | — | B22 |
| 8 | 6–7, 9–16 | B22 | \(c_{4}=0\), \(c_{5}=0\) | OK31, OK13 | OK31 OK13 |
| 9 | 6–7, 9–13 | OK31 | — | — | OK13 |
| 10 | 6–8, 18 | OK13 | — | but atteint | vide |
Le tour 1 traite R11 : les règles 1 et 2 tombent à 0, OK12 et OK21 entrent dans l’agenda. Les tours 2 à 5 traitent les autres faits : O21 et O12 vident la règle 3, qui produit B22 au tour 4 ; C21 et C12 font descendre les règles 4 et 5 à 1, en attente de B22. Les tours 6 et 7 traitent OK12 et OK21, qui ne sont prémisses d’aucune règle. Au tour 8, B22 vide les règles 4 et 5 : OK31 et OK13 entrent. Au tour 9, OK31 est traité sans effet ; au tour 10, OK13 sort de l’agenda, égal au but : succès. Neuf symboles ont été traités, dont OK12, OK21 et OK31, inutiles pour répondre à la question. Les figures montrent le tour 8 et l’état final.
La sortie est :
R11 O21 C21 O12 C12 OK12 OK21 B22 OK31 TrueChaque ajout à l’agenda est un modus ponens : la procédure est correcte. Sur une base de clauses définies, elle est complète pour les symboles : tout symbole conséquence de la base finit dans l’agenda. Elle est linéaire : chaque symbole est traité une fois, chaque prémisse décrémentée une fois. Hors des clauses de Horn, elle est incomplète : une règle à conclusion disjonctive comme \(O_{2,1}\to B_{2,2}\lor B_{3,1}\) ne se laisse pas « déclencher ».
Exemple pas à pas : le chaînage arrière
Le chaînage arrière part du but : un but est établi s’il est un fait, ou s’il est la conclusion d’une règle dont toutes les prémisses sont établies, récursivement. Il est dirigé par le but ; c’est le mécanisme de Prolog.
def prouver(q, pile=()):
print("but :", q)
if q in FAITS:
return True
if q in pile:
return False
for pr, c in REGLES:
if c != q:
continue
pile2 = pile + (q,)
if all(prouver(p, pile2) for p in pr):
return True
return False
print(prouver("OK13"))La fonction prouver affiche le but (ligne 2), le rend vrai s’il est un fait (lignes 3 et 4), le refuse s’il est déjà dans la pile des buts en cours (lignes 5 et 6), et cherche sinon une règle qui le conclut (lignes 7 à 9) pour en prouver les prémisses (ligne 11).
| Appel | Lignes | but | pile | établi par |
|---|---|---|---|---|
| 1 | 2–3, 5, 7–11 | OK13 | vide | règle 5 : B22, C12 |
| 2 | 2–3, 5, 7–11 | B22 | OK13 | règle 3 : O21, O12 |
| 3 | 2–4, 11 | O21 | OK13 B22 | fait |
| 4 | 2–4, 11–12 | O12 | OK13 B22 | fait |
| 5 | 2–4 | C12 | OK13 | fait |
OK13 n’est pas un fait ; la règle 5 le conclut, de prémisses B22 et C12. B22 n’est pas un fait ; la règle 3 le conclut, de prémisses O21 et O12, deux faits : B22 est prouvé à l’appel 4. C12 est un fait : OK13 est prouvé. Cinq buts examinés, aucun symbole inutile : ni OK12, ni OK21, ni OK31. Les figures montrent l’appel 4 et l’état final.
La sortie est :
but : OK13
but : B22
but : O21
but : O12
but : C12
TrueAvec les règles \(P\to Q\) et \(Q\to P\), prouver \(P\) demande \(Q\), qui demande \(P\) : sans le test de la ligne 5, la récursion ne termine pas. La pile des buts en cours l’empêche, au prix d’une recherche plus longue. Le chaînage arrière peut aussi répéter le même sous-but dans deux branches ; mémoriser les buts déjà prouvés ou réfutés le rend linéaire.
| chaînage avant | chaînage arrière | |
|---|---|---|
| direction | des faits vers les conclusions | du but vers les faits |
| dirigé par | les données | le but |
| sur la base de Bouki | 9 symboles traités avant OK13 | 5 buts examinés |
| coût | linéaire en la taille de la base | limité aux buts utiles |
| risque | conclusions inutiles | boucles, d’où la pile des buts |
| usage | surveillance, systèmes de production | Prolog, diagnostic (MYCIN) |
Les deux procédures sont correctes et, sur des clauses définies, complètes pour les symboles ; elles diffèrent par ce qu’elles calculent en route. Le chaînage avant convient à un agent qui surveille (chaque percept nouveau déclenche les déductions qu’il permet) ; le chaînage arrière, à un agent qui répond à une question.
La résolution
La règle de résolution
De deux clauses qui contiennent deux littéraux complémentaires, \(\ell\lor A\) et \(\neg\ell\lor B\) (\(A\) et \(B\) disjonctions, éventuellement vides), la règle de résolution tire la résolvante \(A\lor B\) : \[\frac{\ell\lor A\qquad\neg\ell\lor B}{A\lor B}\] Si \(A\) et \(B\) sont vides, la résolvante est la clause vide : \(\dfrac{P \neg P}{\square}\).
La règle est correcte : dans un modèle des deux clauses, si \(\ell\) est vrai, \(B\) doit l’être, sinon \(A\) l’est ; \(A\lor B\) est donc vraie. Elle contient le modus ponens : \(\neg O_{2,1}\lor B_{2,2}\) et \(O_{2,1}\) donnent \(B_{2,2}\). Elle contient aussi la preuve par cas qui manquait : \(P\lor Q\) et \(\neg P\lor R\) donnent \(Q\lor R\), puis avec \(\neg Q\lor R\), la clause \(R\lor R\), soit \(R\). Le programme représente une clause par un ensemble de littéraux ("~B22" pour \(\neg B_{2,2}\)) : l’ensemble absorbe les doublons, \(R\lor R\) devient \(R\). Les résolvantes qui contiennent un littéral et sa négation sont des tautologies, vraies dans tout monde ; elles n’apportent rien et sont écartées.
def neg(l):
return l[1:] if l.startswith("~") else "~" + l
def fmt(c):
tri = sorted(c, key=lambda l: l.lstrip("~"))
return " | ".join(tri) or "[]"
def resolvantes(ci, cj):
out = []
for l in sorted(ci):
if neg(l) in cj:
r = (ci - {l}) | (cj - {neg(l)})
if not any(neg(x) in r for x in r):
out.append(r)
return out
def noter(r, c, d):
print(fmt(r), ":", fmt(c), "+", fmt(d))
print([fmt(r) for r in resolvantes(frozenset({"~O21", "B22"}),
frozenset({"O21"}))])La sortie est :
['B22']La preuve par réfutation
\(\mathrm{KB}\models\alpha\) si et seulement si \(\mathrm{KB}\land\neg\alpha\) est insatisfiable.
Pour prouver \(\alpha\), on ajoute sa négation à la base, on met le tout en FNC, et on résout des paires de clauses en ajoutant les résolvantes nouvelles. Si la clause vide apparaît, \(\mathrm{KB}\land\neg\alpha\) est insatisfiable (la résolution est correcte, et \(\square\) n’a pas de modèle) : \(\mathrm{KB}\models\alpha\). Si plus aucune résolvante nouvelle n’apparaît sans que \(\square\) ait été obtenue, \(\mathrm{KB}\not\models\alpha\).
Résoudre toutes les paires produit vite un grand nombre de clauses ; une stratégie choisit les paires. La stratégie de l’ensemble de support ne résout que des paires dont l’une des clauses vient du but nié ou de ses descendantes : la recherche reste centrée sur la question. Wos, Robinson et Carson ont montré en 1965 qu’elle reste complète pour la réfutation dès que la base KB est satisfiable, ce qui est le cas d’une base qui décrit un monde réel.
Exemple pas à pas : la réfutation
La base reprend la vérification de modèles en clauses : les deux odeurs et les trois clauses d’unicité. La question est \(\alpha=B_{2,2}\) ; le but nié est \(\neg B_{2,2}\).
KB = [frozenset(c) for c in [
{"B22", "B31"}, {"B13", "B22"}, # odeurs
{"~B13", "~B22"}, {"~B13", "~B31"}, # un seul Bouki
{"~B22", "~B31"}]]
print([fmt(c) for c in KB])| n° | clause | origine |
|---|---|---|
| 1 | \(B_{2,2}\lor B_{3,1}\) | KB |
| 2 | \(B_{1,3}\lor B_{2,2}\) | KB |
| 3 | \(\neg B_{1,3}\lor \neg B_{2,2}\) | KB |
| 4 | \(\neg B_{1,3}\lor \neg B_{3,1}\) | KB |
| 5 | \(\neg B_{2,2}\lor \neg B_{3,1}\) | KB |
| 6 | \(\neg B_{2,2}\) | but nié |
def refutation(kb, but_nie):
traitees = list(kb)
support = [but_nie]
while support:
c = support.pop(0)
for d in traitees:
for r in resolvantes(c, d):
if not r:
noter(r, c, d)
return True
if r not in traitees + support:
support.append(r)
noter(r, c, d)
traitees.append(c)
return False
print(refutation(KB, frozenset({"~B22"})))traitees contient les clauses déjà résolues avec tout ce qui les précède ; support, la file des clauses issues du but nié. À chaque tour, la ligne 5 retire la tête du support et la résout avec chaque clause traitée (lignes 6 et 7). Une résolvante vide arrête la preuve (lignes 8 à 10) ; une résolvante nouvelle entre dans le support et s’affiche (lignes 12 et 13). La clause est enfin rangée parmi les traitées (ligne 14).
| Tour | clause traitée | résolvantes nouvelles (parents) | support après le tour |
|---|---|---|---|
| 1 | 6 : \(\neg B_{2,2}\) | \(B_{3,1}\) (7 = 6 + 1) ; \(B_{1,3}\) (8 = 6 + 2) | \(B_{3,1}\), \(B_{1,3}\) |
| 2 | 7 : \(B_{3,1}\) | \(\neg B_{1,3}\) (9 = 7 + 4) | \(B_{1,3}\), \(\neg B_{1,3}\) |
| 3 | 8 : \(B_{1,3}\) | \(\neg B_{3,1}\) (10 = 8 + 4) | \(\neg B_{1,3}\), \(\neg B_{3,1}\) |
| 4 | 9 : \(\neg B_{1,3}\) | \(B_{2,2}\) (11 = 9 + 2) ; \(\square\) (= 9 + 8) | \(\neg B_{3,1}\), \(B_{2,2}\) |
Au tour 1, \(\neg B_{2,2}\) coupe le littéral \(B_{2,2}\) des deux odeurs : \(B_{3,1}\) et \(B_{1,3}\). Le raisonnement suit alors l’intuition : si Bouki n’est pas en \((2,2)\), il est en \((3,1)\) et en \((1,3)\) à la fois. Aux tours 2 et 3, chacune de ces clauses, avec l’unicité \(\neg B_{1,3}\lor\neg B_{3,1}\), produit la négation de l’autre. Au tour 4, \(\neg B_{1,3}\) rencontre d’abord la clause 2 (et produit \(B_{2,2}\)), puis la clause 8, \(B_{1,3}\) : la clause vide. \(\mathrm{KB}\land\neg B_{2,2}\) est insatisfiable : \(\mathrm{KB}\models B_{2,2}\). Les figures montrent le tour 2 et la fin ; l’arbre résume la preuve.
La sortie est :
B31 : ~B22 + B22 | B31
B13 : ~B22 + B13 | B22
~B13 : B31 + ~B13 | ~B31
~B31 : B13 + ~B13 | ~B31
B22 : ~B13 + B13 | B22
[] : ~B13 + B13
True
Correction, complétude et coût
La résolution est correcte : toute résolvante est conséquence de ses deux parents, donc si \(\square\) est dérivée, l’ensemble de clauses est insatisfiable. Elle est complète pour la réfutation : de tout ensemble insatisfiable de clauses, la saturation par résolution dérive \(\square\). En logique propositionnelle, les clauses possibles sur \(n\) symboles sont en nombre fini (\(3^n\), chaque symbole étant absent, positif ou négatif) : la saturation termine, et la réfutation est une procédure de décision.
La résolution ne dérive pas toute conséquence : de la clause \(P\), aucune résolution ne tire \(P\lor Q\), qui en est pourtant conséquence. Elle établit \(P\lor Q\) en réfutant sa négation, \(\neg P\land\neg Q\), soit les deux clauses \(\neg P\) et \(\neg Q\) : avec \(P\), la première donne \(\square\). C’est pourquoi on l’emploie toujours sous forme de réfutation.
La complétude ne dit rien du coût. Sur la même base de six clauses, la saturation de toutes les paires, chaque clause nouvelle résolue avec toutes celles qui la précèdent, produit 9 clauses nouvelles avant \(\square\) ; l’ensemble de support en produit 5. Sur une base réaliste, l’écart se compte en ordres de grandeur : l’exercice 1 en donne un exemple. Les stratégies classiques sont l’ensemble de support, la préférence unitaire (résoudre d’abord avec des clauses d’un seul littéral) et la résolution linéaire ; sur des clauses de Horn, la résolution linéaire dirigée par le but (résolution SLD) est le chaînage arrière de Prolog.
Le problème SAT et les solveurs
Décider si une formule en FNC est satisfiable est le problème SAT, le premier démontré NP-complet (Cook, 1971) ; décider la validité est co-NP-complet. Aucun algorithme connu ne le résout en temps polynomial dans le pire cas. L’algorithme DPLL (1962) explore les interprétations partielles avec retour arrière, en affectant d’abord les littéraux imposés par une clause unitaire (propagation unitaire) et les littéraux purs (de même signe partout). Les solveurs actuels y ajoutent l’apprentissage de clauses de conflit : ils traitent des instances de millions de variables, en vérification de circuits, en planification ou en ordonnancement. La fonction satisfiable de SymPy utilise un algorithme de type DPLL (ou le solveur pycosat s’il est installé) ; elle confirme la conséquence :
from sympy import satisfiable
B13 = symbols("B13")
base = And(Or(B22, B31), Or(B13, B22), Not(And(B13, B22)),
Not(And(B13, B31)), Not(And(B22, B31)))
for m in satisfiable(base, all_models=True):
print(sorted(m.items(), key=str))
print(satisfiable(And(base, Not(B22))))La sortie est :
[(B13, False), (B22, True), (B31, False)]
FalseLa base a un seul modèle, où \(B_{2,2}\) est vrai, et \(\mathrm{KB}\land\neg B_{2,2}\) n’en a aucun.
La logique du premier ordre
Les limites de la logique propositionnelle
La logique propositionnelle ne parle que de faits particuliers. La règle de l’odeur doit s’écrire 16 fois, une par case ; l’unicité de Bouki demande \(\binom{16}{2}=120\) clauses \(\neg B_{i,j}\lor\neg B_{k,l}\) ; une grotte \(10\times10\) demanderait 100 règles et 4 950 clauses. À l’UCAD, « tout étudiant inscrit paie ses droits » demande une implication par étudiant. Il manque des objets, des relations entre objets, et une manière de dire « pour tout ». La logique du premier ordre (LPO) les apporte : \(\forall x\,(\mathit{Inscrit}(x)\to\mathit{Paie}(x))\) dit en une formule ce qu’il fallait dire par milliers.
Le vocabulaire
Les constantes désignent des objets (\(\mathit{Fatou}\), \(\mathit{Dakar}\), \(\mathit{IA}\)), les variables des objets quelconques (\(x\), \(y\), \(z\)). Un terme est une constante, une variable, ou l’application d’une fonction à des termes, \(f(t_1,\ldots,t_n)\) : \(\mathit{pere}(\mathit{Fatou})\) désigne une personne. Un atome applique un prédicat à des termes : \(\mathit{Enseigne}(\mathit{DrToure},\mathit{IA})\) est vrai ou faux. Les formules se construisent à partir des atomes, des connecteurs, de l’égalité et des quantificateurs \(\forall\) (pour tout) et \(\exists\) (il existe).
Une fonction rend un objet, un prédicat une valeur de vérité : \(\mathit{pere}(\mathit{Fatou})\) est un terme, \(\mathit{Etudiant}(\mathit{Fatou})\) une formule ; \(\mathit{Etudiant}(\mathit{pere}(\mathit{Fatou}))\) dit que le père de Fatou est étudiant.
Les quantificateurs
\(\forall x\,\varphi\) est vraie si \(\varphi\) est vraie pour tout objet du domaine : un seul contre-exemple la rend fausse. \(\exists x\,\varphi\) est vraie si \(\varphi\) est vraie pour au moins un objet : un seul témoin la rend vraie. Une variable est liée si elle est sous la portée d’un quantificateur qui la nomme, libre sinon ; une formule sans variable libre est close. Dans \(\forall x\,(\mathit{Etudiant}(x)\to\mathit{Aime}(x,y))\), \(x\) est liée et \(y\) libre : la formule n’a pas de valeur tant que \(y\) n’est pas fixé.
\(\forall x\,(\mathit{Etudiant}(x)\to\mathit{Paie}(x))\) dit que tout étudiant paie. \(\forall x\,(\mathit{Etudiant}(x)\land\mathit{Paie}(x))\) dit que tout objet du domaine, salles et cours compris, est un étudiant qui paie. À l’inverse, \(\exists x\,(\mathit{Etudiant}(x)\land\mathit{Boursier}(x))\) dit qu’un étudiant boursier existe ; \(\exists x\,(\mathit{Etudiant}(x)\to\mathit{Boursier}(x))\) est vraie dès qu’un objet n’est pas étudiant, l’implication étant alors vraie.
L’ordre des quantificateurs compte. \(\forall x\,\exists y\,\mathit{Inscrit}(x,y)\) dit que chacun suit un cours, pas forcément le même ; \(\exists y\,\forall x\,\mathit{Inscrit}(x,y)\), qu’un même cours réunit tout le monde. La seconde entraîne la première, pas l’inverse. Sur un domaine fini, \(\forall\) est un all et \(\exists\) un any :
ETUDIANTS = ["Fatou", "Amadou", "Awa"]
COURS = ["IA", "ML"]
INSCRIT = {("Fatou", "IA"), ("Amadou", "IA"), ("Awa", "ML")}
# pour tout x, il existe y : Inscrit(x, y)
print(all(any((x, y) in INSCRIT for y in COURS) for x in ETUDIANTS))
# il existe y, pour tout x : Inscrit(x, y)
print(any(all((x, y) in INSCRIT for x in ETUDIANTS) for y in COURS))La sortie est :
True
FalseFatou et Amadou suivent IA, Awa suit ML : chacun suit un cours, aucun cours n’est commun aux trois. Les quantificateurs obéissent à une dualité, analogue des lois de De Morgan : \(\neg\forall x\,\varphi\equiv\exists x\,\neg\varphi\) et \(\neg\exists x\,\varphi\equiv\forall x\,\neg\varphi\). « Il est faux que tous les étudiants réussissent » s’écrit \(\neg\forall x\,(\mathit{Etudiant}(x)\to\mathit{Reussit}(x))\), soit \(\exists x\,(\mathit{Etudiant}(x)\land\neg\mathit{Reussit}(x))\) : en traversant le \(\forall\), la négation transforme \(\to\) en \(\land\).
Interprétation
Une interprétation (ou structure) fixe un domaine \(D\) non vide, un objet de \(D\) pour chaque constante, une fonction de \(D^n\) dans \(D\) pour chaque fonction d’arité \(n\), et une relation \(\subseteq D^n\) pour chaque prédicat d’arité \(n\). La conséquence logique se définit comme en logique propositionnelle : \(\mathrm{KB}\models\alpha\) si toute interprétation qui rend vraie KB rend vraie \(\alpha\).
Avec \(D=\{\mathit{Fatou},\mathit{Amadou},\mathit{DrToure},\mathit{IA},\mathit{ML}\}\) et \(\mathit{Enseigne}=\{(\mathit{DrToure},\mathit{IA})\}\), l’atome \(\mathit{Enseigne}(\mathit{DrToure},\mathit{IA})\) est vrai et \(\mathit{Enseigne}(\mathit{Fatou},\mathit{ML})\) faux. Les domaines peuvent être infinis ; les interprétations ne s’énumèrent plus, et la décision doit passer par les formules.
Le Monde de Bouki en logique du premier ordre
Les cases deviennent des objets, notés \([i,j]\). Trois formules remplacent les 16 règles d’odeur, les 16 règles de brise et les 120 clauses d’unicité : \[\forall c\,(\mathit{Odeur}(c)\leftrightarrow\exists d\,(\mathit{Voisine}(c,d)\land\mathit{Bouki}(d))),\qquad\forall c\,(\mathit{Brise}(c)\leftrightarrow\exists d\,(\mathit{Voisine}(c,d)\land\mathit{Puits}(d))),\] \[\forall c\,\forall d\,((\mathit{Bouki}(c)\land\mathit{Bouki}(d))\to c=d),\] avec \(\mathit{Voisine}([i,j],[k,l])\leftrightarrow|i-k|+|j-l|=1\) et les percepts \(\neg\mathit{Odeur}([1,1])\), \(\mathit{Odeur}([2,1])\), \(\mathit{Odeur}([1,2])\). La taille de la base ne dépend plus de la grille ; le prix à payer est la perte de la décision par énumération.
Forme clausale et unification
Forme prénexe et skolémisation
Pour appliquer la résolution au premier ordre, il faut des clauses ; les quantificateurs doivent disparaître.
Une formule est en forme prénexe si tous ses quantificateurs sont en tête (le préfixe), suivis d’une formule sans quantificateur (la matrice).
\((\forall x\,P(x))\to(\exists y\,Q(y))\) devient \(\neg\forall x\,P(x)\lor\exists y\,Q(y)\), puis, par dualité, \(\exists x\,\neg P(x)\lor\exists y\,Q(y)\), et enfin \(\exists x\,\exists y\,(\neg P(x)\lor Q(y))\) : « il existe un objet sans la propriété \(P\), ou un objet avec la propriété \(Q\) ». Quand deux quantificateurs portent le même nom de variable, il faut d’abord renommer : \((\forall x\,P(x))\land(\exists x\,Q(x))\) devient \((\forall x\,P(x))\land(\exists y\,Q(y))\), puis \(\forall x\,\exists y\,(P(x)\land Q(y))\).
Dans une formule prénexe, chaque \(\exists y\) est supprimé et \(y\) remplacé par une fonction de Skolem nouvelle, appliquée aux variables des \(\forall\) qui le précèdent ; si aucun \(\forall\) ne le précède, par une constante de Skolem nouvelle.
« Il existe un \(y\) » signifie qu’on peut choisir \(y\) ; si ce choix dépend des variables universelles qui précèdent, \(y\) est une fonction de ces variables. \(\forall x\,\exists y\,\mathit{Aime}(x,y)\) (chacun aime quelqu’un) devient \(\forall x\,\mathit{Aime}(x,f(x))\), où \(f(x)\) est « la personne que \(x\) aime ». \(\exists y\,\forall x\,\mathit{Aime}(x,y)\) (quelqu’un est aimé de tous) devient \(\forall x\,\mathit{Aime}(x,c)\), où \(c\) est cette personne.
La formule skolémisée n’est pas équivalente à l’originale : elle affirme davantage, puisqu’elle nomme le témoin. Elle est équisatisfiable : elle a un modèle si et seulement si l’originale en a un. C’est exactement ce dont la réfutation a besoin, puisqu’elle ne teste que l’insatisfiabilité de \(\mathrm{KB}\land\neg\alpha\). La négation du but doit être faite avant la skolémisation : un \(\exists\) du but devient un \(\forall\) après négation.
La forme clausale
- Éliminer \(\leftrightarrow\) et \(\to\).
- Porter les négations sur les atomes (De Morgan, dualité des quantificateurs).
- Renommer les variables : un nom par quantificateur.
- Mettre en forme prénexe.
- Skolémiser.
- Supprimer les \(\forall\) : toute variable restante est universelle.
- Distribuer \(\lor\) sur \(\land\).
- Séparer les clauses, et renommer leurs variables : deux clauses n’en partagent aucune.
« Tout étudiant a un encadrant qui est professeur » s’écrit \(\forall x\,(\mathit{Etudiant}(x)\to\exists y\,(\mathit{Prof}(y)\land\mathit{Encadre}(y,x)))\). Les étapes 1 à 4 donnent \(\forall x\,\exists y\,(\neg\mathit{Etudiant}(x)\lor(\mathit{Prof}(y)\land\mathit{Encadre}(y,x)))\) ; \(y\) dépend de \(x\), la skolémisation le remplace par \(f(x)\) ; la distribution donne deux clauses : \[C_1=\neg\mathit{Etudiant}(x)\lor\mathit{Prof}(f(x)),\qquad C_2=\neg\mathit{Etudiant}(x)\lor\mathit{Encadre}(f(x),x).\] \(f(x)\) est « l’encadrant de \(x\) » : le témoin de l’existentielle est devenu un terme calculé à partir de \(x\).
Substitution et unificateur le plus général
En logique propositionnelle, \(P\) et \(\neg P\) sont complémentaires. Au premier ordre, \(\mathit{Etudiant}(x)\) et \(\neg\mathit{Etudiant}(\mathit{Awa})\) le deviennent si l’on remplace \(x\) par \(\mathit{Awa}\) : c’est le rôle de l’unification.
Une substitution \(\theta=\{x_1/t_1,\ldots,x_n/t_n\}\) remplace simultanément chaque variable \(x_i\) par le terme \(t_i\) ; \(E\theta\) est le résultat. \(\theta\) est un unificateur de \(E_1\) et \(E_2\) si \(E_1\theta=E_2\theta\).
\(\theta\) est un unificateur le plus général (UPG) de \(E_1\) et \(E_2\) si tout unificateur \(\sigma\) de \(E_1\) et \(E_2\) s’écrit \(\sigma=\theta\lambda\) : \(\theta\), puis une substitution \(\lambda\). Deux expressions unifiables ont un UPG, unique à un renommage des variables près (Robinson, 1965).
\(P(x)\) et \(P(y)\) ont pour UPG \(\{x/y\}\) ; \(\{x/\mathit{Fatou},y/\mathit{Fatou}\}\) les unifie aussi, mais il s’obtient de \(\{x/y\}\) en appliquant ensuite \(\{y/\mathit{Fatou}\}\), et il est moins général : il fixe une valeur que rien n’impose. La résolution utilise l’UPG pour garder les conclusions les plus générales.
Dans le code, une variable est une chaîne qui commence par une minuscule, une constante par une majuscule, et un terme composé est un tuple (symbole, arguments). lier pose une liaison \(v/t\) en suivant les liaisons déjà posées, et la refuse si \(v\) apparaît dans \(t\) : c’est le test d’occurrence, que réalise apparait.
def est_var(t):
return isinstance(t, str) and t[0].islower()
def compose(t):
return isinstance(t, tuple)
def lier(v, t, s):
if v in s:
return unifier(s[v], t, s)
if est_var(t) and t in s:
return unifier(v, s[t], s)
if apparait(v, t, s):
return None # test d'occurrence
return {**s, v: t}def apparait(v, t, s):
if t == v:
return True
if est_var(t) and t in s:
return apparait(v, s[t], s)
if compose(t):
return any(apparait(v, u, s)
for u in t[1:])
return FalseExemple pas à pas : l’unification
Il s’agit d’unifier les deux atomes suivants, « \(x\) accompagne son père chez \(y\) » et « Fatou accompagne \(z\) chez \(z\) » : \[E_1=\mathit{Accompagne}(x,\mathit{pere}(x),y),\qquad E_2=\mathit{Accompagne}(\mathit{Fatou},z,z).\]
def unifier(a, b, s):
if s is None:
return None
if a == b:
return s
if est_var(a):
return lier(a, b, s)
if est_var(b):
return lier(b, a, s)
if not compose(a) or not compose(b):
return None
if a[0] != b[0] or len(a) != len(b):
return None
for x, y in zip(a[1:], b[1:]):
s = unifier(x, y, s)
return s
E1 = ("Accompagne", "x", ("pere", "x"), "y")
E2 = ("Accompagne", "Fatou", "z", "z")
print(unifier(E1, E2, {}))unifier reçoit deux expressions et la substitution courante \(s\). Elle rend \(s\) si les expressions sont égales (lignes 4 et 5), lie une variable (lignes 6 à 9), échoue si l’une des expressions n’est pas composée (lignes 10 et 11) ou si les symboles ou les arités diffèrent (lignes 12 et 13), et unifie sinon les arguments un à un, en propageant \(s\) (lignes 14 et 15).
| Appel | \(a\) | \(b\) | \(s\) reçue | décision |
|---|---|---|---|---|
| 1 | E1 | E2 | \(\emptyset\) | même symbole, arité 3 : arguments un à un (ligne 15) |
| 2 | x |
Fatou |
\(\emptyset\) | \(x\) variable (ligne 6) : \(x/\mathit{Fatou}\) |
| 3 | pere(x) |
z |
\(\{x/\mathit{Fatou}\}\) | \(z\) variable (ligne 8), absent de \(\mathit{pere}(x)\) : \(z/\mathit{pere}(x)\) |
| 4 | y |
z |
\(\{x/\mathit{Fatou}, z/\mathit{pere}(x)\}\) | \(y\) variable, \(z\) déjà lié : lier reprend avec \(\mathit{pere}(x)\) |
| 5 | y |
pere(x) |
\(\{x/\mathit{Fatou}, z/\mathit{pere}(x)\}\) | \(y\) variable (ligne 6) : \(y/\mathit{pere}(x)\) |
L’appel 1 compare deux termes composés de même symbole et de même arité. Les arguments sont unifiés dans l’ordre : \(x\) avec \(\mathit{Fatou}\) (appel 2), puis \(\mathit{pere}(x)\) avec \(z\) (appel 3) : \(z\) est une variable qui n’apparaît pas dans \(\mathit{pere}(x)\), d’où \(z/\mathit{pere}(x)\). À l’appel 4, \(y\) fait face à \(z\), déjà lié : lier reprend avec la valeur de \(z\), \(\mathit{pere}(x)\), et l’appel 5 lie \(y\). Les figures montrent l’appel 3 et la fin.
La sortie est :
{'x': 'Fatou', 'z': ('pere', 'x'), 'y': ('pere', 'x')}Le dictionnaire rendu est triangulaire : \(z/\mathit{pere}(x)\) contient \(x\), lui-même lié à \(\mathit{Fatou}\). L’appliquer jusqu’au bout donne l’UPG :
def appliquer(t, s):
if est_var(t) and t in s:
return appliquer(s[t], s)
if isinstance(t, tuple):
return (t[0],) + tuple(appliquer(x, s) for x in t[1:])
return t
s = unifier(E1, E2, {})
print({v: appliquer(v, s) for v in sorted(s)})
print(appliquer(E1, s) == appliquer(E2, s))La sortie est :
{'x': 'Fatou', 'y': ('pere', 'Fatou'), 'z': ('pere', 'Fatou')}
TrueL’UPG est \(\{x/\mathit{Fatou},\ y/\mathit{pere}(\mathit{Fatou}),\ z/\mathit{pere}(\mathit{Fatou})\}\) : « Fatou accompagne son père chez lui ».
Les échecs de l’unification
print(unifier(("Aime", "x", "x"), ("Aime", "Awa", "Fatou"), {}))
print(unifier(("Parent", "x", ("f", "x")), ("Parent", "y", "y"), {}))
print(unifier(("Inscrit", "x", "IA"), ("Inscrit", "Awa", "y"), {}))La sortie est :
None
None
{'x': 'Awa', 'y': 'IA'}\(\mathit{Aime}(x,x)\) et \(\mathit{Aime}(\mathit{Awa},\mathit{Fatou})\) ne s’unifient pas : \(x/\mathit{Awa}\), puis \(\mathit{Awa}\) face à \(\mathit{Fatou}\), deux constantes distinctes. C’est un conflit de symboles, pas un échec du test d’occurrence. \(\mathit{Parent}(x,f(x))\) et \(\mathit{Parent}(y,y)\) ne s’unifient pas non plus : \(x/y\), puis \(y\) face à \(f(y)\). Ici, c’est le test d’occurrence : \(y\) apparaît dans \(f(y)\), et aucune substitution finie ne rend \(y\) égal à \(f(y)\) (il faudrait \(y=f(f(f(\ldots)))\)). La troisième paire s’unifie par \(\{x/\mathit{Awa},y/\mathit{IA}\}\).
Prolog omet par défaut le test d’occurrence, coûteux : il lie \(y\) à \(f(y)\) et peut alors « prouver » une conclusion qui n’est pas une conséquence de la base. La résolution n’est correcte qu’avec ce test.
La résolution au premier ordre
Soient deux clauses sans variable commune, \(\ell\lor A\) et \(\neg m\lor B\), telles que les atomes \(\ell\) et \(m\) aient un UPG \(\theta\). La résolvante est \((A\lor B)\theta\).
\(\neg\mathit{Etudiant}(x)\lor\mathit{Prof}(f(x))\) et \(\mathit{Etudiant}(\mathit{Awa})\) ont pour UPG \(\{x/\mathit{Awa}\}\) ; la résolvante est \(\mathit{Prof}(f(\mathit{Awa}))\) : l’encadrant d’Awa est professeur. C’est le modus ponens généralisé : une règle universelle appliquée à un cas.
Avec la factorisation (unifier deux littéraux de même signe d’une même clause, pour n’en garder qu’un), la résolution est correcte et complète pour la réfutation au premier ordre (Robinson, 1965) : si \(\mathrm{KB}\models\alpha\), la réfutation de \(\mathrm{KB}\land\neg\alpha\) finit par dériver \(\square\). Mais la conséquence logique du premier ordre n’est que semi-décidable (Church, Turing, 1936) : si \(\mathrm{KB}\not\models\alpha\), la recherche peut ne jamais s’arrêter, les termes \(f(c)\), \(f(f(c))\), … formant une infinité de clauses possibles. Les démonstrateurs comme Vampire ou E reposent sur la résolution et ses descendants, avec des stratégies qui la guident ; Prolog la restreint aux clauses de Horn, explorées en profondeur.
Systèmes experts et calcul symbolique
Les systèmes experts
Les systèmes experts sont l’application la plus connue de l’IA symbolique : des agents fondés sur les connaissances dont la base contient le savoir d’un expert, écrit en règles.
MYCIN, développé à Stanford dans les années 1970 (thèse d’Edward Shortliffe), conseillait le traitement des infections bactériennes graves, bactériémies puis méningites. Il comptait environ 600 règles, un moteur en chaînage arrière, et des facteurs de certitude entre \(-1\) et \(+1\) pour les règles incertaines. Sur des cas de méningite, ses prescriptions, évaluées à l’aveugle par huit infectiologues, ont été jugées acceptables dans 65 % des 80 évaluations (10 cas, 8 évaluateurs), contre 42,5 à 62,5 % pour cinq médecins de la faculté. Les facteurs de certitude sortent de la logique classique : ils annoncent les probabilités de la Séance 5.
Au centre de santé de la Médina, à Dakar, un système expert minimal relie symptômes et conduites à tenir. Les règles portent sur un patient quelconque ; elles sont appliquées à chaque patient par saturation, une forme de chaînage avant.
REGLES_M = [(["fievre", "frissons", "pluies"], "suspect_palu"),
(["fievre", "toux", "rhinite"], "suspect_grippe"),
(["suspect_palu"], "TDR"), (["suspect_grippe"], "repos")]
def diagnostic(faits):
connus = set(faits)
nouveau = True
while nouveau:
nouveau = False
for pr, c in REGLES_M:
if set(pr) <= connus and c not in connus:
connus.add(c)
nouveau = True
return sorted(connus - set(faits))
palu = ["fievre", "frissons", "pluies"]
print("Fatou :", diagnostic(palu))
print("Moussa :", diagnostic(palu + ["toux", "rhinite"]))La sortie est :
Fatou : ['TDR', 'suspect_palu']
Moussa : ['TDR', 'repos', 'suspect_grippe', 'suspect_palu']L’incertitude. Moussa présente les symptômes des deux règles : le système conclut paludisme et grippe, sans pouvoir dire lequel est le plus probable. La logique classique n’a pas de degré ; le théorème de Bayes (Séance 5) en donnera. L’acquisition des connaissances. Chaque règle s’obtient d’un expert, par entretiens ; c’est un travail long, coûteux et jamais complet, le goulot d’étranglement de l’acquisition des connaissances. Le Machine Learning le contourne en apprenant les règles, ou les probabilités, à partir des données.
Calcul symbolique
Le calcul symbolique, ou calcul formel, manipule des expressions mathématiques comme des symboles, en leur appliquant des règles de réécriture : la dérivée d’une somme est la somme des dérivées, la dérivée de \(\sin\) est \(\cos\), celle de \(x^2\) est \(2x\). C’est un raisonnement sur des symboles, au même titre que l’inférence logique : le système part d’une expression et applique des règles jusqu’à une forme réduite. Son résultat est exact, et valable pour tout \(x\) ; le calcul numérique, lui, rend une approximation en un point.
from sympy import sin, cos, diff, integrate, simplify, solve, Eq
x = symbols("x")
f = x**2 + sin(x)
print(diff(f, x))
print(integrate(f, x))
g = lambda t: float(f.subs(x, t))
num = (g(0.501) - g(0.5)) / 0.001
exact = float(diff(f, x).subs(x, 0.5))
print(round(num, 6), round(exact, 6))La sortie est :
2*x + cos(x)
x**3/3 - cos(x)
1.878343 1.877583La dérivée formelle de \(x^2+\sin x\) est \(2x+\cos x\) ; en \(x=0{,}5\), elle vaut \(1{,}877583\). Le quotient différentiel avec \(h=0{,}001\) donne \(1{,}878343\) : l’écart, environ \(\frac h2f''(x)\), est de l’ordre de \(h\). SymPy résout aussi des équations et simplifie. Un étudiant dépense 50 000 francs CFA par mois en transport \(t\) et repas \(r\) ; si le transport doublait, la dépense serait de 80 000. Le système \(t+r=50\,000\), \(2t+r=80\,000\) se résout ainsi :
print(simplify((x + 1)**2 - x**2 - 1))
print(solve(x**2 - 5*x + 6, x))
t, r = symbols("t r")
eqs = [Eq(t + r, 50000), Eq(2*t + r, 80000)]
sol = solve(eqs, [t, r])
print(sol[t], sol[r])La sortie est :
2*x
[2, 3]
30000 20000Le module de logique de SymPy réalise les opérations de cette séance : simplification, mise en FNC, satisfiabilité.
from sympy import simplify_logic, Implies
P, Q, R = symbols("P Q R")
print(simplify_logic(Or(And(P, Q), And(P, Not(Q)))))
print(simplify_logic(Implies(P, Implies(Q, P))))
phi = Implies(Or(P, Q), And(R, Not(P)))
print(to_cnf(phi))
print(to_cnf(phi, simplify=True))
print(satisfiable(And(P, Implies(P, Q), Not(Q))))La sortie est :
P
True
~P & (R | ~P) & (R | ~Q) & (~P | ~Q)
~P & (R | ~Q)
False\((P\land Q)\lor(P\land\neg Q)\) se réduit à \(P\) ; \(P\to(Q\to P)\) est valide, réduite à True. La FNC de \((P\lor Q)\to(R\land\neg P)\) rendue par défaut compte quatre clauses, dont \(\neg P\lor R\), absorbée par \(\neg P\) ; avec simplify=True, il en reste deux : une formule a plusieurs FNC équivalentes. Enfin \(P\land(P\to Q)\land\neg Q\) est insatisfiable : c’est la réfutation qui prouve le modus ponens.
Exercices corrigés
Les trois exercices reprennent les trois raisonnements que demandent le TD et le TP : une mise en FNC suivie d’une preuve par réfutation, présentée en table numérotée ; les chaînages avant et arrière déroulés sur une même base, en table des tours ; une mise en forme clausale au premier ordre, suivie d’unifications et d’une résolution qui extrait une réponse.
Exercice 1 : la sûreté de la case \((3,1)\)
Ousmane a perçu : rien en \((1,1)\) ; une odeur et pas de brise en \((2,1)\) ; une odeur et pas de brise en \((1,2)\). Le départ ne contient ni Bouki ni puits ; Bouki n’occupe qu’une case.
- Écrire les règles du monde pour l’odeur en \((2,1)\), l’odeur en \((1,2)\), la brise en \((2,1)\) et la brise en \((1,2)\), puis l’unicité restreinte aux trois cases \((1,3)\), \((2,2)\) et \((3,1)\).
- Mettre la règle de l’odeur en \((1,2)\) en FNC, en nommant chaque étape.
- Prouver \(\neg P_{3,1}\) par réfutation.
- Prouver \(\neg B_{3,1}\) par réfutation, en donnant la table des clauses. Combien de résolvantes le programme de la section Section 6 produit-il sur les 14 clauses de l’odeur et de l’unicité, rangées dans l’ordre : règle de \((2,1)\), règle de \((1,2)\), \(O_{2,1}\), \(O_{1,2}\), \(\neg B_{1,1}\), unicité ?
- Prouver de même que \((1,3)\) est sûre pour Bouki. Conclure.
Méthode. Écrire chaque règle en équivalence (le percept dans un sens, la cause dans l’autre), passer en clauses, ajouter la négation de ce que l’on veut prouver, puis résoudre en commençant par les clauses d’un seul littéral : faits, percepts, négation du but.
(a) Odeur en \((2,1)\) : \(O_{2,1}\leftrightarrow(B_{1,1}\lor B_{2,2}\lor B_{3,1})\) ; odeur en \((1,2)\) : \(O_{1,2}\leftrightarrow(B_{1,1}\lor B_{1,3}\lor B_{2,2})\) ; brise en \((2,1)\) : \(\mathit{Br}_{2,1}\leftrightarrow(P_{1,1}\lor P_{2,2}\lor P_{3,1})\) ; brise en \((1,2)\) : \(\mathit{Br}_{1,2}\leftrightarrow(P_{1,1}\lor P_{1,3}\lor P_{2,2})\). Les percepts sont \(O_{2,1}\), \(O_{1,2}\), \(\neg\mathit{Br}_{2,1}\), \(\neg\mathit{Br}_{1,2}\) ; le départ, \(\neg B_{1,1}\) et \(\neg P_{1,1}\). L’unicité : \(\neg B_{1,3}\lor\neg B_{2,2}\), \(\neg B_{1,3}\lor\neg B_{3,1}\), \(\neg B_{2,2}\lor\neg B_{3,1}\) (au plus un des trois).
(b) Étape 1 : \((O_{1,2}\to B_{1,1}\lor B_{1,3}\lor B_{2,2})\land(B_{1,1}\lor B_{1,3}\lor B_{2,2}\to O_{1,2})\). Étape 2 : \((\neg O_{1,2}\lor B_{1,1}\lor B_{1,3}\lor B_{2,2})\land(\neg(B_{1,1}\lor B_{1,3}\lor B_{2,2})\lor O_{1,2})\). Étape 3 : \(\neg(B_{1,1}\lor B_{1,3}\lor B_{2,2})\) devient \(\neg B_{1,1}\land\neg B_{1,3}\land\neg B_{2,2}\). Étape 4 : \((\neg B_{1,1}\land\neg B_{1,3}\land\neg B_{2,2})\lor O_{1,2}\) se distribue en trois clauses. FNC : \((\neg O_{1,2}\lor B_{1,1}\lor B_{1,3}\lor B_{2,2})\land(\neg B_{1,1}\lor O_{1,2})\land(\neg B_{1,3}\lor O_{1,2})\land(\neg B_{2,2}\lor O_{1,2})\), quatre clauses, comme pour \((2,1)\).
(c) La règle de la brise donne de même quatre clauses ; on ajoute le percept \(\neg\mathit{Br}_{2,1}\) et la négation du but, \(P_{3,1}\). La réfutation par ensemble de support (le programme de la section Section 6) donne :
| n° | clause | origine |
|---|---|---|
| 1 | \(\neg \mathit{Br}_{2,1}\lor P_{1,1}\lor P_{2,2}\lor P_{3,1}\) | KB |
| 2 | \(\mathit{Br}_{2,1}\lor \neg P_{1,1}\) | KB |
| 3 | \(\mathit{Br}_{2,1}\lor \neg P_{2,2}\) | KB |
| 4 | \(\mathit{Br}_{2,1}\lor \neg P_{3,1}\) | KB |
| 5 | \(\neg \mathit{Br}_{2,1}\) | KB |
| 6 | \(P_{3,1}\) | négation de \(\neg P_{3,1}\) |
| 7 | \(\mathit{Br}_{2,1}\) | 6 + 4 |
| 8 | \(P_{1,1}\lor P_{2,2}\lor P_{3,1}\) | 7 + 1 |
| 9 | \(\square\) | 7 + 5 |
\(P_{3,1}\) et \(\neg P_{3,1}\lor\mathit{Br}_{2,1}\) donnent \(\mathit{Br}_{2,1}\) ; avec le percept \(\neg\mathit{Br}_{2,1}\), la clause vide. La clause 8, produite au passage avec la première clause de la règle, ne sert pas : le programme résout avec les clauses traitées dans leur ordre. \(\neg P_{3,1}\) est prouvé : pas de puits en \((3,1)\). C’est un modus tollens : un puits en \((3,1)\) ferait sentir une brise en \((2,1)\).
(d) On ajoute \(B_{3,1}\) (négation de \(\neg B_{3,1}\)) et on résout en préférant les clauses d’un littéral. Les six clauses de la forme \(\neg B\lor O\) sont inutiles et omises.
| n° | clause | origine |
|---|---|---|
| 1 | \(B_{1,1}\lor B_{2,2}\lor B_{3,1}\lor \neg O_{2,1}\) | règle de \((2,1)\) |
| 2 | \(B_{1,1}\lor B_{1,3}\lor B_{2,2}\lor \neg O_{1,2}\) | règle de \((1,2)\) |
| 3 | \(O_{2,1}\) | percept |
| 4 | \(O_{1,2}\) | percept |
| 5 | \(\neg B_{1,1}\) | départ sûr |
| 6 | \(\neg B_{1,3}\lor \neg B_{2,2}\) | unicité |
| 7 | \(\neg B_{1,3}\lor \neg B_{3,1}\) | unicité |
| 8 | \(\neg B_{2,2}\lor \neg B_{3,1}\) | unicité |
| 9 | \(B_{3,1}\) | négation de \(\neg B_{3,1}\) |
| 10 | \(B_{1,1}\lor B_{1,3}\lor B_{2,2}\) | 2 + 4, sur \(O_{1,2}\) |
| 11 | \(B_{1,3}\lor B_{2,2}\) | 10 + 5, sur \(B_{1,1}\) |
| 12 | \(\neg B_{1,3}\) | 9 + 7, sur \(B_{3,1}\) |
| 13 | \(\neg B_{2,2}\) | 9 + 8, sur \(B_{3,1}\) |
| 14 | \(B_{2,2}\) | 11 + 12, sur \(B_{1,3}\) |
| 15 | \(\square\) | 14 + 13, sur \(B_{2,2}\) |
Le percept \(O_{1,2}\) réduit la règle de \((1,2)\) à \(B_{1,1}\lor B_{1,3}\lor B_{2,2}\) (clause 10), le départ sûr à \(B_{1,3}\lor B_{2,2}\) (clause 11) : Bouki est en \((1,3)\) ou en \((2,2)\). La négation du but, avec l’unicité, interdit les deux : \(\neg B_{1,3}\) (12) et \(\neg B_{2,2}\) (13). La clause 11 et la clause 12 donnent \(B_{2,2}\), qui contredit 13 : \(\square\). La règle de \((2,1)\) ne sert pas : l’odeur en \((1,2)\) et l’unicité excluent à elles seules \((3,1)\), puisque Bouki doit être voisin de \((1,2)\) et que \((3,1)\) ne l’est pas.
Sur les 14 clauses rangées dans l’ordre de l’énoncé, plus la négation du but, le programme produit 159 résolvantes avant la clause vide, contre 5 pour la preuve ci-dessus, qui ne résout qu’avec des clauses d’un littéral ; le nombre dépend aussi de l’ordre des clauses. L’ordre des résolutions ne change pas le verdict ; il change le coût.
(e) On ajoute \(B_{1,3}\), numérotée 9 à la place de \(B_{3,1}\) ; les clauses 1 à 8 sont celles de (d) :
| n° | clause | origine |
|---|---|---|
| 10 | \(\neg B_{2,2}\) | 9 + 6 |
| 11 | \(\neg B_{3,1}\) | 9 + 7 |
| 12 | \(B_{1,1}\lor B_{2,2}\lor B_{3,1}\) | 1 + 3 |
| 13 | \(B_{2,2}\lor B_{3,1}\) | 12 + 5 |
| 14 | \(B_{3,1}\) | 13 + 10 |
| 15 | \(\square\) | 14 + 11 |
Avec l’unicité, \(B_{1,3}\) donne \(\neg B_{2,2}\) (10) et \(\neg B_{3,1}\) (11) ; la règle de \((2,1)\) et le percept \(O_{2,1}\) donnent \(B_{1,1}\lor B_{2,2}\lor B_{3,1}\) (12), réduit par le départ sûr à \(B_{2,2}\lor B_{3,1}\) (13) ; avec 10 puis 11, la clause vide. Comme en (c), la clause \(\mathit{Br}_{1,2}\lor\neg P_{1,3}\) et le percept \(\neg\mathit{Br}_{1,2}\) réfutent \(P_{1,3}\) : \(P_{1,3}\) donne \(\mathit{Br}_{1,2}\), puis \(\square\). Conclusion : \((3,1)\) et \((1,3)\) sont sûres ; Ousmane peut y entrer.
Erreur fréquente. Ajouter le but lui-même au lieu de sa négation : avec \(\neg B_{3,1}\) ajouté, la base reste satisfiable, aucune clause vide n’apparaît, et l’on conclut à tort à l’échec. Autre erreur : oublier l’unicité, sans laquelle ni \(\neg B_{3,1}\) ni \(\neg B_{1,3}\) ne sont des conséquences.
Exercice 2 : la pompe solaire du forage de Linguère
Un agent surveille la pompe solaire d’un forage pastoral de Linguère. Ses règles, dans cet ordre : (1) \(\mathit{filtre\_bouche}\to\mathit{debit\_faible}\) ; (2) \(\mathit{soleil}\land\mathit{panneaux\_sales}\to\mathit{tension\_faible}\) ; (3) \(\mathit{tension\_faible}\to\mathit{debit\_faible}\) ; (4) \(\mathit{tension\_faible}\to\mathit{nettoyer}\) ; (5) \(\mathit{debit\_faible}\land\mathit{reservoir\_bas}\to\mathit{alerte}\) ; (6) \(\mathit{nuit}\to\mathit{batterie\_lente}\). Les faits, dans cet ordre : \(\mathit{soleil}\), \(\mathit{panneaux\_sales}\), \(\mathit{nuit}\), \(\mathit{reservoir\_bas}\). Le but est \(\mathit{alerte}\).
- Vérifier que la base est faite de clauses de Horn et l’écrire en clauses.
- Dérouler le chaînage avant : pour chaque tour, le symbole sorti, les compteurs modifiés, les symboles ajoutés et l’agenda.
- Dérouler le chaînage arrière : les buts examinés, dans l’ordre, avec la pile.
- Comparer les deux déroulements.
Méthode. Pour le chaînage avant, tenir l’agenda (une file) et un compteur par règle, initialisé au nombre de prémisses ; un compteur à 0 fait entrer la conclusion. Pour le chaînage arrière, essayer les règles dans l’ordre et prouver les prémisses de gauche à droite ; noter la pile des buts en cours.
(a) Chaque règle a une seule conclusion et des prémisses positives : \(\neg\mathit{debit\_faible}\lor\neg\mathit{reservoir\_bas}\lor\mathit{alerte}\), par exemple, a un seul littéral positif. Les faits sont des clauses d’un littéral positif. La base est de Horn ; les compteurs initiaux sont 1, 2, 1, 1, 2, 1.
(b) La table du chaînage avant, calculée par le programme de la section Section 5 :
| Tour | sort | compteurs | ajouté | agenda après le tour |
|---|---|---|---|---|
| 1 | soleil |
\(c_{2}=1\) | — | panneaux_sales nuit reservoir_bas |
| 2 | panneaux_sales |
\(c_{2}=0\) | tension_faible |
nuit reservoir_bas tension_faible |
| 3 | nuit |
\(c_{6}=0\) | batterie_lente |
reservoir_bas tension_faible batterie_lente |
| 4 | reservoir_bas |
\(c_{5}=1\) | — | tension_faible batterie_lente |
| 5 | tension_faible |
\(c_{3}=0\), \(c_{4}=0\) | debit_faible, nettoyer |
batterie_lente debit_faible nettoyer |
| 6 | batterie_lente |
— | — | debit_faible nettoyer |
| 7 | debit_faible |
\(c_{5}=0\) | alerte |
nettoyer alerte |
| 8 | nettoyer |
— | — | alerte |
| 9 | alerte |
— | but atteint | vide |
Les quatre premiers tours traitent les faits : \(\mathit{panneaux\_sales}\) vide la règle 2, qui fait entrer \(\mathit{tension\_faible}\) ; \(\mathit{nuit}\) vide la règle 6 ; \(\mathit{reservoir\_bas}\) fait passer la règle 5 à 1. Au tour 5, \(\mathit{tension\_faible}\) vide les règles 3 et 4 : \(\mathit{debit\_faible}\) et \(\mathit{nettoyer}\) entrent. Au tour 7, \(\mathit{debit\_faible}\) vide la règle 5 : \(\mathit{alerte}\) entre, et sort au tour 9, égal au but. La règle 1 reste à 1 : \(\mathit{filtre\_bouche}\) n’est jamais établi.
(c) La table du chaînage arrière :
| Appel | but | pile | établi par |
|---|---|---|---|
| 1 | alerte |
vide | règle 5 |
| 2 | debit_faible |
alerte |
règle 1 échoue, règle 3 |
| 3 | filtre_bouche |
alerte debit_faible |
ni fait ni règle : échec |
| 4 | tension_faible |
alerte debit_faible |
règle 2 |
| 5 | soleil |
alerte debit_faible tension_faible |
fait |
| 6 | panneaux_sales |
alerte debit_faible tension_faible |
fait |
| 7 | reservoir_bas |
alerte |
fait |
\(\mathit{alerte}\) demande la règle 5, donc \(\mathit{debit\_faible}\) puis \(\mathit{reservoir\_bas}\). Pour \(\mathit{debit\_faible}\), la règle 1 est essayée la première : \(\mathit{filtre\_bouche}\) n’est ni un fait ni la conclusion d’une règle, l’appel 3 échoue ; la règle 3 est alors essayée, et \(\mathit{tension\_faible}\) se prouve par la règle 2 et deux faits. \(\mathit{reservoir\_bas}\) est un fait : succès en 7 appels.
(d) Le chaînage avant traite 8 symboles avant le but, dont \(\mathit{batterie\_lente}\) et \(\mathit{nettoyer}\), inutiles pour l’alerte (mais utiles à un agent qui surveille : « nettoyer » est une action à conseiller). Le chaînage arrière examine 7 buts, dont un échec (\(\mathit{filtre\_bouche}\)) : il ne regarde jamais la règle 6 ni le fait \(\mathit{nuit}\), mais il paie l’essai d’une règle qui ne mène à rien. Les deux concluent \(\mathit{alerte}\) ; sur une base de Horn, ils sont corrects et complets.
Erreur fréquente. Dans le chaînage avant, décrémenter un compteur deux fois pour la même prémisse, ou déclencher une règle dès qu’une de ses prémisses est connue : une règle ne se déclenche que lorsque son compteur atteint 0. Dans le chaînage arrière, s’arrêter au premier échec : l’échec de la règle 1 renvoie à la règle suivante qui conclut le même but.
Exercice 3 : les pirogues de Joal
Au quai de pêche de Joal : (1) toute pirogue a un capitaine : \(\forall x\,(\mathit{Pirogue}(x)\to\exists y\,\mathit{Capitaine}(y,x))\) ; (2) tout capitaine d’une pirogue a un permis : \(\forall x\,\forall y\,(\mathit{Capitaine}(y,x)\to\mathit{Permis}(y))\) ; (3) \(\mathit{Sopi}\) est une pirogue.
- Mettre (1) et (2) en forme clausale.
- Écrire la négation du but « quelqu’un a un permis », \(\exists z\,\mathit{Permis}(z)\), en clause.
- Conduire la résolution, en donnant à chaque pas les clauses, l’UPG et la résolvante.
- Quelle personne la preuve désigne-t-elle ?
- Unifier \(\mathit{Capitaine}(y,y)\) et \(\mathit{Capitaine}(f(x),x)\). Que signifie le résultat ?
Méthode. Mettre la base et la négation du but en clauses, renommer les variables de chaque clause, puis résoudre en partant du but nié ; à chaque pas, calculer l’UPG des deux littéraux complémentaires et l’appliquer à toute la résolvante.
(a) (1) : éliminer \(\to\), \(\forall x\,(\neg\mathit{Pirogue}(x)\lor\exists y\,\mathit{Capitaine}(y,x))\) ; forme prénexe \(\forall x\,\exists y\,(\neg\mathit{Pirogue}(x)\lor\mathit{Capitaine}(y,x))\) ; \(y\) dépend de \(x\) : \(y\mapsto f(x)\), « le capitaine de \(x\) » ; clause \(K_1=\neg\mathit{Pirogue}(x)\lor\mathit{Capitaine}(f(x),x)\). (2) : \(K_2=\neg\mathit{Capitaine}(y,x)\lor\mathit{Permis}(y)\). (3) : \(K_3=\mathit{Pirogue}(\mathit{Sopi})\).
(b) \(\neg\exists z\,\mathit{Permis}(z)\equiv\forall z\,\neg\mathit{Permis}(z)\) : clause \(\neg\mathit{Permis}(z)\). La négation précède la skolémisation : le \(\exists\) du but devient un \(\forall\), il n’y a pas de fonction de Skolem.
(c) La résolution par ensemble de support, l’unification étant celle de la section Section 8 :
| Pas | clause du support | clause de KB (renommée) | UPG | résolvante |
|---|---|---|---|---|
| 1 | \(\neg \mathit{Permis}(z)\) | \(\neg \mathit{Capitaine}(y, x) \lor \mathit{Permis}(y)\) | \(\{z/y\}\) | \(\neg \mathit{Capitaine}(y, x)\) |
| 2 | \(\neg \mathit{Capitaine}(y, x)\) | \(\neg \mathit{Pirogue}(x') \lor \mathit{Capitaine}(f(x'), x')\) | \(\{x/x', y/f(x')\}\) | \(\neg \mathit{Pirogue}(x')\) |
| 3 | \(\neg \mathit{Pirogue}(x')\) | \(\mathit{Pirogue}(\mathit{Sopi})\) | \(\{x'/\mathit{Sopi}\}\) | \(\square\) |
Pas 1 : \(\mathit{Permis}(z)\) et \(\mathit{Permis}(y)\) s’unifient par \(\{z/y\}\) ; il reste \(\neg\mathit{Capitaine}(y,x)\). Pas 2 : les variables de \(K_1\) sont renommées (\(x\) devient \(x'\)), puisque \(x\) figure déjà dans la clause du support ; \(\mathit{Capitaine}(y,x)\) et \(\mathit{Capitaine}(f(x'),x')\) s’unifient par \(\{y/f(x'),x/x'\}\) ; il reste \(\neg\mathit{Pirogue}(x')\). Pas 3 : \(\{x'/\mathit{Sopi}\}\), et la clause vide.
(d) En composant les substitutions : \(z/y\), \(y/f(x')\), \(x'/\mathit{Sopi}\), d’où \(z=f(\mathit{Sopi})\), le capitaine de la pirogue Sopi. La preuve ne dit pas qui il est : elle établit qu’il existe et qu’il a un permis ; la fonction de Skolem le nomme.
(e) L’unification du programme donne :
| Appel | \(a\) | \(b\) | \(s\) reçue |
|---|---|---|---|
| 1 | Capitaine(y, y) |
Capitaine(f(x), x) |
\(\emptyset\) |
| 2 | y |
f(x) |
\(\emptyset\) |
| 3 | y |
x |
\(\{y/f(x)\}\) |
| 4 | f(x) |
x |
\(\{y/f(x)\}\) |
\(y/f(x)\), puis \(y\), déjà lié, face à \(x\) : il faut unifier \(f(x)\) et \(x\), et \(x\) apparaît dans \(f(x)\) ; le test d’occurrence fait échouer l’unification. « \(y\) est capitaine de \(y\), et \(y\) est le capitaine de \(x\), qui est \(x\) » demanderait \(x=f(x)\), un objet capitaine de lui-même : aucune substitution finie ne convient.
Erreur fréquente. Skolémiser le but avant de le nier : \(\exists z\,\mathit{Permis}(z)\) deviendrait \(\mathit{Permis}(c)\), puis \(\neg\mathit{Permis}(c)\), qui ne s’unifie avec rien d’utile, et la preuve échoue. Autre erreur : oublier de renommer. Ici le hasard fait que \(\mathit{Capitaine}(y,x)\) et \(\mathit{Capitaine}(f(x),x)\) s’unifient quand même, par \(\{y/f(x)\}\). Mais si \(K_1\) avait été écrite avec la variable \(y\), \(\neg\mathit{Pirogue}(y)\lor\mathit{Capitaine}(f(y),y)\), la paire \(\mathit{Capitaine}(y,x)\) / \(\mathit{Capitaine}(f(y),y)\) échouerait par le test d’occurrence (\(y/f(y)\)), alors que les clauses renommées s’unifient.
À retenir
- Un agent fondé sur les connaissances : une base de formules, TELL pour ajouter, ASK pour inférer, un moteur indépendant du domaine.
- Une interprétation donne une valeur à chaque symbole ; un modèle rend la formule vraie. Satisfiable, valide, insatisfiable ; \(\mathrm{KB}\models\alpha\) si et seulement si \(\mathrm{Mod}(\mathrm{KB})\subseteq\mathrm{Mod}(\alpha)\), si et seulement si \(\mathrm{KB}\land\neg\alpha\) est insatisfiable.
- La vérification de modèles est correcte et complète, en \(2^n\).
- FNC en quatre étapes (éliminer \(\leftrightarrow\), \(\to\), porter les négations, distribuer) ; clauses de Horn : au plus un littéral positif.
- \(\vdash\) est syntaxique, \(\models\) sémantique ; correcte : \(\vdash\) entraîne \(\models\) ; complète : \(\models\) entraîne \(\vdash\).
- Sur des clauses définies, le chaînage avant (dirigé par les données, linéaire) et le chaînage arrière (dirigé par le but, avec une pile contre les boucles) sont corrects et complets pour les symboles.
- La résolution est correcte et complète pour la réfutation ; une stratégie (ensemble de support, préférence unitaire) en réduit le coût ; SAT est NP-complet.
- Au premier ordre : \(\forall\) avec \(\to\), \(\exists\) avec \(\land\) ; skolémisation équisatisfiable, après la négation du but ; UPG, test d’occurrence ; résolution avec unification et factorisation, complète pour la réfutation ; \(\models\) semi-décidable.
- Ousmane déduit Bouki en \((2,2)\) de deux odeurs et de l’unicité, puis que \((3,1)\) et \((1,3)\) sont sûres ; les systèmes experts appliquent ces mécanismes à des règles d’expert, le calcul symbolique à des expressions mathématiques.
Prochaine séance
Ousmane sait désormais quelles cases sont sûres ; la logique ne lui dit pas quel chemin prendre jusqu’à l’or. La Séance 3, « L’IA qui cherche », formule un problème de recherche (états, actions, coûts, but) et le résout par les algorithmes BFS, DFS, UCS, A* et la recherche locale, sur la route de Dakar à Touba : comment un agent trouve-t-il une suite d’actions qui mène à son but ?
Références
- Russell, S., Norvig, P. — Artificial Intelligence: A Modern Approach, 4e éd., Pearson, 2020 (chap. 7 à 9).
- Poole, D., Mackworth, A. — Artificial Intelligence: Foundations of Computational Agents, 3e éd., Cambridge University Press, 2023.
- Robinson, J. A. — « A Machine-Oriented Logic Based on the Resolution Principle », Journal of the ACM, 12(1), 1965.
- Davis, M., Logemann, G., Loveland, D. — « A Machine Program for Theorem-Proving », Communications of the ACM, 5(7), 1962.
- Buchanan, B., Shortliffe, E. — Rule-Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project, Addison-Wesley, 1984.
- Ben-Ari, M. — Mathematical Logic for Computer Science, 3e éd., Springer, 2012.
- Meurer, A. et al. — « SymPy: Symbolic Computing in Python », PeerJ Computer Science, 3, 2017.
Pour cette séance
Les slides
À lire en ligne
À télécharger
- Code de départ du TP (ZIP, 4 Ko)