Agents logiques et planification

Un agent à base de connaissances agit à partir d'une description de son monde. Sa base de connaissances (KB) contient des formules formelles : des faits et des règles initiaux, appelés axiomes, ainsi que des informations ajoutées pendant son fonctionnement. L'inférence relie ces formules à des conclusions que l'agent n'a jamais observées directement.

Relier la perception à l'action

TELL ajoute une formule à la base de connaissances. ASK demande une réponse qui en découle, déjà stockée ou déduite. À chaque instant, l'agent enregistre sa perception, demande quelle action entreprendre, enregistre l'action choisie et l'exécute. L'enregistrement des actions est important, car les raisonnements ultérieurs doivent tenir compte des changements du monde.

Au niveau des connaissances, on peut dire qu'un robot sait qu'un passage est bloqué et veut atteindre une zone de stockage. Au niveau de l'implémentation, on décrit les structures de données et les procédures d'inférence. Une conception déclarative fournit des faits et des règles ; une conception procédurale écrit directement le comportement dans le code. Un agent opérationnel peut combiner les deux.

Comprendre le monde du wumpus

Le monde du wumpus est une grille de 4 × 4 cases. Les coordonnées sont [colonne, ligne] ; l'agent commence en [1, 1], tourné vers la droite. Il y a un wumpus, une pièce d'or et une probabilité de 0,2 de trouver un puits dans chaque case sauf celle du départ. Les puits et le wumpus restent immobiles. Le monde est discret, déterministe et comporte un seul agent, mais il est partiellement observable : la disposition des éléments est cachée.

Une Brise indique un puits dans une case directement adjacente ; une Odeur y indique le wumpus. Les cases en diagonale ne comptent pas. Un Reflet indique la présence d'or dans la case courante, un Choc signale un mur et un Cri signale la mort du wumpus partout dans la grotte. Les actions sont Avancer, TournerÀGauche, TournerÀDroite, Ramasser, Tirer et Sortir. L'agent dispose d'une flèche ; Sortir permet de quitter la grotte uniquement depuis [1, 1]. Sortir avec l'or rapporte 1 000 points, mourir en fait perdre 1 000, chaque action coûte 1 et tirer coûte 10 de plus.

Combiner les observations

En [1, 1], l'absence de Brise exclut des puits en [1, 2] et [2, 1] ; l'absence d'Odeur y exclut le wumpus. Les deux cases sont sûres. En [2, 1], une Brise place un puits en [2, 2] ou en [3, 1], puisque la case de départ n'en contient pas. L'absence d'Odeur exclut le wumpus en [2, 2] et [3, 1].

L'agent visite ensuite [1, 2]. L'absence de Brise exclut un puits en [2, 2] : la disjonction précédente impose donc la présence d'un puits en [3, 1]. Une Odeur en [1, 2] place le wumpus en [1, 3] ou en [2, 2]. L'absence d'Odeur observée précédemment exclut [2, 2] ; il reste [1, 3]. L'agent a établi que [2, 2] ne contient aucun des deux dangers sans y entrer.

Ce raisonnement repose à la fois sur les perceptions et sur les règles qui les relient aux dangers. Une case inexplorée est de statut inconnu lorsque la base de connaissances ne permet d'établir ni qu'elle est sûre ni qu'elle est dangereuse. Ne pas parvenir à déduire un danger ne suffit pas pour affirmer qu'elle est sûre. Choisir d'entrer dans une telle case nécessite une décision sur le risque, au-delà des seules conséquences logiques.

La logique propositionnelle donne à un agent des règles précises pour combiner des affirmations auxquelles on peut répondre par oui ou par non. Un symbole atomique désigne une affirmation entière, comme P₁₂ pour « il y a un puits en [1, 2] ». Un littéral est une formule atomique ou sa négation. Des formules plus grandes les combinent avec ¬, ∧, ∨, ⇒ et ⇔.

Évaluer les connecteurs

Un modèle attribue la valeur vrai ou faux à chaque symbole. Avec n symboles, il existe 2ⁿ affectations. La négation inverse une valeur de vérité ; une conjonction exige que ses deux membres soient vrais ; une disjonction inclusive exige qu'au moins l'un d'eux soit vrai. Une implication n'est fausse que si sa prémisse est vraie et sa conclusion fausse. Une biconditionnelle exige que les valeurs de vérité de ses deux membres soient égales.

L'ordre de priorité est ¬, ∧, ∨, ⇒, ⇔. Ainsi, ¬A ∧ B ⇒ C signifie ((¬A) ∧ B) ⇒ C. Utilise des parenthèses lorsque le regroupement voulu pourrait être ambigu. Avec A vraie, B fausse et C vraie, (A ∨ B) ⇒ C est vraie, tandis que A ⇒ (B ∧ C) est fausse.

L'implication logique énonce une contrainte sur les valeurs de vérité, pas une cause. Une prémisse fausse rend l'implication vraie. Elle ne permet pas non plus d'inverser le sens : à partir de « si la batterie est vide, le robot s'arrête », le seul arrêt du robot ne permet pas d'établir que la batterie est vide.

Encoder les deux sens d'une règle

La règle de la brise à la case de départ est B₁₁ ⇔ (P₁₂ ∨ P₂₁). Elle dit qu'une brise apparaît exactement lorsqu'une case voisine contient un puits. Le sens B₁₁ ⇒ (P₁₂ ∨ P₂₁) permet de détecter un danger à partir d'une brise. Le sens inverse permet d'exclure des puits en l'absence de brise. L'omettre fait perdre l'inférence de ¬B₁₁ à ¬P₁₂ ∧ ¬P₂₁.

Chaque case doit avoir sa propre règle propositionnelle. Encoder exactement un wumpus parmi 16 cases nécessite une disjonction imposant au moins un wumpus et une contrainte imposant au plus un wumpus pour chaque paire. Il existe 16 × 15 / 2 = 120 paires distinctes. Les symboles propositionnels ne peuvent pas quantifier sur les cases : les règles générales deviennent donc de nombreuses formules distinctes.

Représenter le changement sans perdre la persistance

Un fluent est un fait dont la vérité peut changer. Un exposant temporel distingue ses valeurs : L₁₁⁰ indique la position à l'instant 0. Un axiome d'effet peut dire qu'un déplacement vers la droite depuis [1, 1] produit la position [2, 1] à l'instant 1 et supprime l'ancienne position. Il ne précise pas ce qu'il advient des faits sans rapport, comme la possession de la flèche. Décrire tous ces faits inchangés constitue le problème du cadre.

Un axiome d'état successeur donne une règle complète de mise à jour par fluent : Fᵗ⁺¹ ⇔ (une action rend F vrai) ∨ (Fᵗ ∧ aucune action ne rend F faux). Pour la flèche, HaveArrowᵗ⁺¹ ⇔ (HaveArrowᵗ ∧ ¬Shootᵗ). Comme aucune action ne fournit une autre flèche, l'agent la conserve jusqu'au tir et ne l'a plus ensuite.

Un agent a besoin d'un critère pour déterminer si une conclusion est justifiée. La conséquence logique, notée KB ⊨ α, signifie que α est vraie dans tout modèle qui satisfait la base de connaissances. Un seul monde compatible où α est fausse suffit à invalider cette conséquence logique.

Ne garder que les modèles compatibles

La vérification des modèles énumère les affectations, écarte celles qui rendent fausse une formule de la base et teste la requête dans celles qui restent. Supposons que la base contienne A ∨ B et ¬A. Parmi les quatre affectations de A et B, seule A faux, B vrai satisfait les deux formules. B et ¬A sont des conséquences logiques de la base. A n'en est pas une, car le modèle restant rend A fausse.

Dans la base du wumpus, ¬P₁₁, B₁₁ ⇔ (P₁₂ ∨ P₂₁), B₂₁ ⇔ (P₁₁ ∨ P₂₂ ∨ P₃₁), ¬B₁₁ et B₂₁ utilisent sept symboles. Il existe 128 affectations. Exactement trois satisfont la base : P₁₂ et P₂₁ sont fausses, tandis que P₂₂ et P₃₁ sont respectivement vraies/fausses, fausses/vraies ou vraies/vraies. Ainsi, ¬P₁₂ est une conséquence logique. P₂₂ varie entre les trois modèles : ni P₂₂ ni ¬P₂₂ n'est donc une conséquence logique. Ces seules règles sur les puits établissent l'absence d'un puits, pas celle du wumpus.

Distinguer les principaux tests logiques

P ∨ ¬P est valide ; P ∧ ¬P est insatisfiable. P ⇒ Q et ¬P ∨ Q sont équivalentes. L'équivalence exige une conséquence logique dans les deux sens. A ∧ B implique logiquement A, mais A admet des modèles où B est fausse : la conséquence logique inverse ne tient donc pas.

Transformer une requête en test de contradiction

KB ⊨ α exactement lorsque KB ∧ ¬α est insatisfiable. Ajouter la négation de la requête revient à chercher un monde où la base est vraie et la requête fausse. N'en trouver aucun démontre la conséquence logique ; en trouver un donne un contre-modèle. De manière équivalente, α ⊨ β exactement lorsque α ⇒ β est valide. La validité de α peut elle-même être vérifiée en déterminant si ¬α est insatisfiable.

Le connecteur ⇒ figure à l'intérieur d'une formule. Le symbole ⊨ décrit une relation entre des formules et leurs modèles. De même, « n'est pas une conséquence logique » peut signifier que la requête est exclue ou qu'elle reste inconnue. Vérifie si sa négation est une conséquence logique avant de choisir entre les deux.

L'énumération est correcte et complète en logique propositionnelle, car elle vérifie exhaustivement un ensemble fini. L'énumération en profondeur prend un temps O(2ⁿ) et une mémoire O(n) ; 50 symboles donnent déjà environ 1,13 × 10¹⁵ affectations. La conséquence logique propositionnelle est co-NP-complète. Vérifie aussi la cohérence : une base sans modèle implique logiquement toute formule, car elle n'a aucun modèle compatible qui pourrait rendre une requête fausse.

Une preuve déduit une requête en appliquant des règles à des formules déjà connues. KB ⊢ α indique une déduction ; KB ⊨ α indique une garantie sémantique portant sur les modèles. Une procédure de preuve correcte relie les deux : toute conclusion qu'elle déduit découle réellement des prémisses. Une procédure complète peut déduire toute conclusion qui est une conséquence logique dans le langage considéré.

Appliquer les règles à leurs prémisses

Le modus ponens permet de passer de P ⇒ Q et P à Q. L'élimination de la conjonction permet de passer de P ∧ Q à l'un ou l'autre de ses membres. Si SensorOn ∧ Calibrated est connue et que SensorOn ⇒ ReadingAvailable est connue, l'élimination de la conjonction donne SensorOn, puis le modus ponens donne ReadingAvailable. Chaque ligne indique les informations et la règle qui la justifient.

Ces règles préservent la vérité, mais les formes limitées qu'elles manipulent les rendent incomplètes en tant que système de preuve. De P, la formule P ∨ Q découle sémantiquement, mais aucune des deux règles n'introduit ∨. Un ensemble de règles correctes peut néanmoins manquer des conclusions valides.

Réécrire sans changer le sens

Des équivalences utiles peuvent être appliquées dans les deux sens :

• Double négation : ¬¬P ≡ P.
• Implication : P ⇒ Q ≡ ¬P ∨ Q.
• Contraposition : P ⇒ Q ≡ ¬Q ⇒ ¬P.
• Biconditionnelle : P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P).
• Lois de De Morgan : ¬(P ∨ Q) ≡ ¬P ∧ ¬Q, et ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.
• Distribution : P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R), avec la loi duale pour ∧ sur ∨.

La conjonction et la disjonction permettent aussi de regrouper et de réordonner leurs éléments. Ces réécritures font apparaître la structure utile d'une formule sans ajouter de nouvelle hypothèse factuelle.

Pour B₁₁ ⇔ (P₁₂ ∨ P₂₁) et ¬B₁₁, sépare la biconditionnelle et choisis (P₁₂ ∨ P₂₁) ⇒ B₁₁. La contraposition donne ¬B₁₁ ⇒ ¬(P₁₂ ∨ P₂₁). Le modus ponens donne ¬(P₁₂ ∨ P₂₁) ; la loi de De Morgan donne ¬P₁₂ ∧ ¬P₂₁. L'élimination de la conjonction démontre alors ¬P₁₂. La preuve n'a jamais besoin d'énumérer toutes les dispositions possibles de la grotte.

Tester un raccourci invalide

De P ⇒ Q et Q, déduire P est une affirmation du conséquent. De P ⇒ Q et ¬P, déduire ¬Q est une négation de l'antécédent. Les deux échouent dans le modèle P faux, Q vrai. Une panne de serveur peut empêcher une page de se charger, mais un échec de chargement peut avoir d'autres causes ; l'absence de panne ne garantit pas non plus le succès du chargement.

La recherche d'une preuve est un problème de recherche. L'état initial contient la base de connaissances ; une action applique une règle d'inférence et ajoute sa conclusion ; l'état but contient la requête. La longueur de la preuve peut servir de coût du chemin. Choisir les formules pertinentes évite de consacrer des efforts à des chaînes sans rapport. La logique classique est monotone : ajouter des prémisses préserve les conséquences logiques antérieures. Les règles par défaut avec exceptions nécessitent un autre traitement, car des informations ultérieures peuvent retirer une conclusion obtenue par défaut.

La résolution démontre une conséquence logique en recherchant une contradiction. Son entrée est une forme normale conjonctive : une conjonction de clauses, chacune étant une disjonction de littéraux. Une clause à un seul littéral est une clause unitaire. La clause vide ne contient aucun littéral susceptible d'être vrai et représente le faux.

Transformer les formules en clauses

Élimine d'abord ⇔ et ⇒. Fais ensuite entrer les négations à l'aide des lois de De Morgan et de l'élimination des doubles négations. Enfin, distribue ∨ sur ∧. Une biconditionnelle peut ainsi produire plusieurs clauses.

Pour B₁₁ ⇔ (P₁₂ ∨ P₂₁), le premier sens donne ¬B₁₁ ∨ P₁₂ ∨ P₂₁. Le sens inverse donne ¬(P₁₂ ∨ P₂₁) ∨ B₁₁. Faire entrer la négation et distribuer donne ¬P₁₂ ∨ B₁₁ et ¬P₂₁ ∨ B₁₁. Les trois clauses sont nécessaires pour représenter toute la biconditionnelle.

Appliquer la résolution à une paire complémentaire

De P ∨ A et ¬P ∨ B, la résolution déduit A ∨ B. Quelle que soit la valeur de P, au moins une des parties restantes doit être vraie. La résolution unitaire utilise une clause à un seul littéral : P avec ¬P ∨ B donne B. Les littéraux répétés sont factorisés : la résolution de A ∨ B avec A ∨ ¬B donne donc A.

Applique la résolution à exactement une paire complémentaire à la fois. A ∨ B et ¬A ∨ ¬B sont satisfiables ensemble lorsque A est vraie et B fausse. Supprimer les deux paires donnerait à tort la clause vide. Appliquer la résolution à A seul produit B ∨ ¬B, une tautologie qui n'ajoute aucune contrainte.

Réfuter la négation de la requête

Pour démontrer KB ⊨ α, ajoute ¬α, transforme la formule obtenue en forme normale conjonctive et déduis de nouvelles clauses par résolution. Obtenir la clause vide démontre qu'il n'existe aucun contre-modèle.

Pour la requête ¬P₁₂ sur le puits, ajoute P₁₂. Applique la résolution avec ¬P₁₂ ∨ B₁₁ pour obtenir B₁₁, puis avec ¬B₁₁, qui a été observée, pour obtenir la clause vide. La preuve établit l'absence du puits, pas sa présence : le littéral positif du puits était la négation temporaire de la requête.

Un deuxième exemple utilise R ⇒ C, (C ∨ I) ⇒ G et R. Les clauses en forme normale conjonctive sont ¬R ∨ C, ¬C ∨ G, ¬I ∨ G et R. Ajoute ¬G. Sa résolution avec ¬C ∨ G donne ¬C, qui donne ¬R avec la première clause. La résolution de ¬R avec R achève la réfutation. Aucun fait concernant I n'était nécessaire.

La résolution propositionnelle est correcte et complète pour la réfutation. Elle se termine parce qu'un nombre fini de symboles permet un nombre fini de clauses distinctes. Si la recherche exhaustive de nouvelles clauses n'en produit plus et ne donne aucune contradiction, la requête n'est pas une conséquence logique. La résolution ne déduit pas nécessairement directement toutes les conséquences logiques : de A seule, elle ne construit pas A ∨ B.

La distribution peut augmenter exponentiellement la taille de la forme normale conjonctive. Un encodage de Tseitin introduit des symboles pour les sous-formules et produit une forme normale conjonctive de taille linéaire. La nouvelle formule est satisfiable exactement lorsque l'initiale l'est ; elle n'est pas nécessairement logiquement équivalente à celle-ci sur le vocabulaire étendu. Préserver la satisfiabilité suffit pour les tests de contradiction fondés sur SAT.

Les règles à une seule conclusion positive permettent une procédure d'inférence plus simple que la résolution générale. Une clause définie contient exactement un littéral positif ; ¬A ∨ ¬B ∨ C s'écrit A ∧ B ⇒ C. Un fait a un corps vide. Une clause de Horn contient au plus un littéral positif, ce qui inclut les clauses de but qui n'en ont aucun, comme A ∧ B ⇒ Faux.

Laisser les faits guider les règles

Le chaînage avant part des faits connus. Lorsque toutes les prémisses d'une règle sont connues, ajoute sa tête. Continue jusqu'à ce que la requête apparaisse ou qu'un point fixe n'ajoute plus rien. Les implémentations efficaces conservent une liste de nouveaux faits à traiter et un compteur des prémisses non satisfaites pour chaque règle.

Prends PowerOn, FanSpinning et LoadLow comme faits. Les règles sont PowerOn ∧ FanSpinning ⇒ Cooling ; Cooling ∧ LoadLow ⇒ TempNormal ; PowerOn ⇒ LedLit ; LedLit ∧ TempNormal ⇒ SystemOK ; FanSpinning ⇒ NoiseHeard. Le traitement de PowerOn permet d'obtenir LedLit et satisfait partiellement la règle de refroidissement. FanSpinning permet d'obtenir Cooling et NoiseHeard. Cooling avec LoadLow donne TempNormal, puis TempNormal avec LedLit donne SystemOK. NoiseHeard est une conclusion supplémentaire valide, même si la requête n'en avait pas besoin.

Laisser une requête choisir les règles

Le chaînage arrière part de SystemOK. Sa règle exige LedLit et TempNormal. LedLit se ramène au fait connu PowerOn. TempNormal exige Cooling et LoadLow ; Cooling exige PowerOn et FanSpinning. Chaque feuille est un fait, donc la requête réussit. La règle relative au bruit n'est jamais examinée.

Pour les bases de clauses définies et les requêtes atomiques, les deux méthodes sont correctes et complètes avec un contrôle approprié de la recherche. Le chaînage avant propositionnel peut s'exécuter en un temps linéaire par rapport à la taille de la base. À son point fixe, attribuer vrai aux symboles déduits et faux à tous les autres donne un modèle des clauses définies.

Gérer les cycles sans perdre de réponses

A ⇒ B et B ⇒ A entraînent une procédure arrière naïve dans une boucle sans fin. Une branche peut s'arrêter lorsque son but figure déjà dans la pile des buts actifs. Les sous-buts démontrés peuvent être mémorisés, mais un échec causé par une boucle est temporaire. Avec B ⇒ A, A ⇒ B, C ⇒ A et le fait C, une première tentative de démontrer B pendant que A est actif peut échouer. Après avoir démontré A à partir de C, une nouvelle tentative pour B réussit. Mémoriser définitivement ce premier échec ferait perdre la preuve. La tabulation suit les buts dépendants et les réexamine lorsque des réponses apparaissent.

Le chaînage dépend de la forme des règles. A ∨ B contient deux littéraux positifs : ce n'est donc pas une clause de Horn. Avec A ⇒ C et B ⇒ C, elle implique logiquement C si l'on considère les deux possibilités. Aucune règle définie ne se déclenche à partir de la seule disjonction. La résolution générale peut démontrer cette conclusion même lorsque le chaînage simple reste bloqué.

Un solveur SAT recherche une affectation qui satisfait toutes les clauses d'une formule en forme normale conjonctive. Un modèle renvoyé peut être vérifié directement. Un résultat d'insatisfiabilité exclut toutes les affectations. SAT est NP-complet, mais les instances structurées admettent souvent des solutions bien plus rapides que l'énumération exhaustive par table de vérité.

Réduire la recherche avec DPLL

DPLL est une recherche en profondeur avec retour arrière et trois raccourcis. Un littéral vrai satisfait toute sa clause, tandis qu'une clause entièrement fausse met fin à la branche. Un symbole pur n'apparaît qu'avec un seul signe parmi les clauses non satisfaites : on peut donc lui attribuer la valeur qui satisfait ces occurrences. Une clause unitaire ne possède plus qu'un seul littéral susceptible d'être vrai, auquel il faut attribuer la valeur vrai. Répéter ces choix imposés constitue la propagation unitaire.

Considère (A), (¬A ∨ B), (¬B ∨ C ∨ D), (¬C ∨ ¬D), (D ∨ E). E est pur, donc pose E vrai. La clause unitaire A impose A vrai, ce qui impose B vrai. La contrainte restante C ∨ D et la clause ¬C ∨ ¬D exigent qu'exactement un de C et D soit vrai. Crée une branche avec C vrai ; la propagation impose D faux. A, B, C et E vrais avec D faux satisfont toutes les clauses.

Pour (A ∨ B), (A ∨ ¬B), (¬A ∨ C), (¬A ∨ ¬C), crée des branches sur A. A faux impose à la fois B et ¬B ; A vrai impose à la fois C et ¬C. Les deux branches aboutissent à un conflit, donc la formule entière est insatisfiable.

Apprendre des conflits

L'apprentissage de clauses dirigé par les conflits, utilisé par CDCL, étend cette recherche. Une clause apprise bloque une combinaison responsable d'un conflit. Le retour arrière non chronologique saute les choix non pertinents ; l'activité des variables guide le branchement ; les redémarrages changent le parcours de recherche ; les littéraux surveillés accélèrent la propagation. Les clauses apprises sont justifiées par la formule et préservent donc ses solutions possibles.

Rechercher en modifiant une affectation complète

WalkSAT part d'une affectation complète aléatoire. Il choisit une clause non satisfaite et inverse une variable de celle-ci, parfois au hasard et parfois de façon à laisser le plus de clauses satisfaites. Les déplacements aléatoires aident à échapper aux pièges locaux. Dans l'exemple précédent, partir avec les cinq symboles faux laisse (A) et (D ∨ E) fausses. Inverser A satisfait (A), mais rend (¬A ∨ B) fausse. Un déplacement peut satisfaire une clause tout en en rendant une autre fausse.

Pour vérifier une conséquence logique, soumets KB ∧ ¬α. L'insatisfiabilité démontre α ; un modèle est un contre-exemple. Si WalkSAT atteint sa limite de temps, les deux possibilités restent ouvertes. Dans les grandes formules aléatoires en forme normale conjonctive à 3 littéraux, le rapport entre clauses et variables présente une transition estimée près de 4,26, avec des instances difficiles souvent proches de ce seuil. C'est une tendance observée sur un ensemble de formules, pas un seuil qui permet de trancher pour une formule donnée. La structure des clauses et la stratégie du solveur influent aussi sur la difficulté.

La logique du premier ordre décrit des objets et leurs relations. Au lieu de donner à chaque case un symbole sans lien avec les autres, elle peut exprimer une règle pour toutes les cases : ∀s (Breezy(s) ⇔ ∃r (Adjacent(r, s) ∧ Pit(r))). Les quantificateurs permettent d'exprimer la généralité dans le langage.

Distinguer les objets des affirmations

Une constante nomme un objet, comme Ada. Une variable, comme x, prend ses valeurs parmi les objets. Une fonction associe des objets à un objet : MotherOf(Ada) est un terme qui désigne une personne. Un prédicat forme une affirmation : Owns(Ada, Atlas) est vraie ou fausse. Un terme peut être une constante, une variable ou une fonction appliquée à des termes.

Book(x) est une formule, pas un objet : Owns(Ada, Book(x)) place donc le mauvais type d'expression à la position d'un argument. L'égalité compare les objets désignés par les termes : MotherOf(Ada) = Clara dit que les deux termes désignent le même objet.

Évaluer une formule dans un modèle

Un modèle du premier ordre fournit un domaine non vide et une interprétation. Les constantes désignent des objets du domaine, les prédicats désignent des relations et les fonctions fournissent un résultat pour chaque tuple approprié d'objets du domaine. Une formule quantifiée universellement doit être vraie pour chaque valeur possible de sa variable ; une formule existentielle nécessite au moins un témoin.

Soit le domaine {a, b, k} ; Ada nomme a, Ben nomme b et Atlas nomme k. Person contient a et b, Book contient k et Owns ne contient que (a, k). Owns(Ada, Atlas) est vraie. ∃x (Book(x) ∧ Owns(Ben, x)) est fausse parce que Ben ne possède aucun objet. ∀x (Person(x) ⇒ ∃y (Book(y) ∧ Owns(x, y))) est fausse parce que Ben est un contre-exemple. Pourtant, chaque livre a un propriétaire : ∀x (Book(x) ⇒ ∃y Owns(y, x)) est vraie.

Expliciter les hypothèses de modélisation

La logique du premier ordre standard n'impose pas ces hypothèses des bases de données. Book(Atlas), Book(Beowulf), Owns(Ada, Atlas) et Owns(Ada, Beowulf) laissent ouverte la possibilité que les deux noms désignent le même livre et qu'Ada possède d'autres livres. Avec la sémantique des bases de données, ces faits décrivent exactement deux livres possédés par Ada.

Pour obtenir cette affirmation précise avec la sémantique standard, conserve les quatre faits et ajoute ¬(Atlas = Beowulf) et ∀x ((Book(x) ∧ Owns(Ada, x)) ⇒ (x = Atlas ∨ x = Beowulf)). L'inégalité établit que les deux livres sont distincts ; la restriction universelle exclut qu'Ada possède d'autres livres.

Les modèles du premier ordre peuvent avoir des domaines arbitrairement grands : la méthode d'énumération finie des modèles propositionnels ne fournit donc pas ici une procédure de décision générale. Les méthodes de preuve travaillent à la place sur la structure des formules. Une variable libre nécessite une affectation pour l'évaluation ; lie les variables lorsque tu écris une affirmation close pour la base de connaissances.

La traduction commence par déterminer ce que la phrase affirme sur chaque objet. La portée des quantificateurs, le sens de l'implication et l'égalité déterminent le sens ; les seuls noms des prédicats ne le fixent pas. Les parenthèses rendent la portée voulue visible.

Utiliser le bon connecteur avec un quantificateur

« Tous les chats sont des mammifères » devient ∀x (Cat(x) ⇒ Mammal(x)). Un objet extérieur à la catégorie satisfait l'implication sans être un chat. Écrire ∀x (Cat(x) ∧ Mammal(x)) affirme à tort que tout est un chat.

« Un chat est noir » devient ∃x (Cat(x) ∧ Black(x)). Le témoin doit satisfaire les deux propriétés. Avec ∃x (Cat(x) ⇒ Black(x)), tout objet qui n'est pas un chat est déjà un témoin, même dans un monde sans chat noir. Les règles universelles sur les catégories utilisent généralement l'implication ; les affirmations existentielles sur les catégories utilisent généralement la conjonction.

Vérifier qui peut dépendre de qui

∀x ∃y Loves(x, y) permet une personne aimée différente pour chaque x. ∃y ∀x Loves(x, y) exige une personne aimée de tous. Dans un monde de deux personnes où chacune n'aime que l'autre, la première formule est vraie et la seconde fausse. Intervertir des quantificateurs de nature différente peut changer une affirmation ; intervertir deux quantificateurs universels adjacents ou deux quantificateurs existentiels adjacents la préserve.

La négation échange les quantificateurs : ¬∀x P(x) ≡ ∃x ¬P(x), et ¬∃x P(x) ≡ ∀x ¬P(x). Par conséquent, « Tous les étudiants n'ont pas réussi » signifie ∃x (Student(x) ∧ ¬Passed(x)). Il faut qu'un étudiant ait échoué ; cela n'affirme pas que tous les étudiants ont échoué.

Exprimer le sens et le nombre

« Seuls les membres empruntent » signifie ∀x (Borrows(x) ⇒ Member(x)). Emprunter suffit à établir l'appartenance, tandis que l'appartenance seule ne dit rien sur l'emprunt. « Aucun reptile n'est un mammifère » signifie ∀x (Reptile(x) ⇒ ¬Mammal(x)).

Pour exprimer qu'Ada possède au moins deux livres, écris ∃x ∃y (Book(x) ∧ Book(y) ∧ Owns(Ada, x) ∧ Owns(Ada, y) ∧ ¬(x = y)). L'inégalité est importante : deux noms de variables peuvent désigner le même objet. Pour exactement un livre, on utilise un témoin et l'unicité : ∃x (Book(x) ∧ Owns(Ada, x) ∧ ∀y ((Book(y) ∧ Owns(Ada, y)) ⇒ y = x)).

Donner les deux sens des définitions

Une définition des frères et sœurs peut être ∀x ∀y (Sibling(x, y) ⇔ (¬(x = y) ∧ ∃p (Parent(p, x) ∧ Parent(p, y)))). Le premier sens impose des conditions aux frères et sœurs ; le sens inverse permet d'établir ce lien à partir des faits sur un parent commun. Une implication à sens unique ne fournit que la moitié de ce sens.

Dans le domaine d'un agent, les règles diagnostiques vont des observations vers les causes possibles, tandis que les règles causales vont des causes vers les effets. « Toute case où l'on perçoit une brise est adjacente à un puits » est diagnostique. « Tout puits provoque une brise dans chaque case adjacente » est causale. Ensemble, elles permettent d'établir la biconditionnelle complète de la brise. Termine une traduction en vérifiant la liaison de chaque variable et en testant un petit monde où l'affirmation française devrait être fausse.

Construire une base de connaissances utile est une tâche de modélisation. La notation formelle n'aide qu'après le choix des questions, des objets et des relations pertinents. L'ingénierie des connaissances transforme ces choix en axiomes que l'on peut vérifier à l'aide d'exemples représentatifs du monde visé.

Construire autour des questions

Une démarche pratique consiste à déterminer la tâche, recueillir les connaissances pertinentes, choisir un vocabulaire, écrire des axiomes généraux, ajouter les faits d'une instance, poser des requêtes et corriger les résultats. Commence par des questions concrètes comme « Cet étudiant peut-il s'inscrire à ce cours ? ». Cette question détermine ce que la représentation doit permettre d'exprimer.

Pour l'inscription, utilise Student(s), Course(c), Prereq(p, c), Passed(s, c) et CanEnroll(s, c). Prereq(p, c) signifie que p doit être validé avant c ; inverser ses arguments inverserait la dépendance. Une règle est ∀s ∀c ((Student(s) ∧ Course(c) ∧ ∀p (Prereq(p, c) ⇒ Passed(s, p))) ⇒ CanEnroll(s, c)). Elle exige que tous les prérequis soient validés, pas seulement un.

Séparer les règles réutilisables d'une instance

Supposons que les faits soient Student(Mia), Course(AI), Prereq(Logic, AI), Prereq(Programming, AI), Passed(Mia, Logic) et Passed(Mia, Programming). La règle générale peut être réutilisée pour d'autres étudiants et cours, tandis que ces faits d'instance décrivent un cas particulier.

En logique du premier ordre standard, ces faits laissent ouverte la possibilité de prérequis supplémentaires pour AI. Un modèle compatible pourrait contenir un troisième prérequis non validé, donc CanEnroll(Mia, AI) n'est pas encore une conséquence logique. Ajoute ∀p (Prereq(p, AI) ⇔ (p = Logic ∨ p = Programming)) pour compléter la liste. Désormais, chaque prérequis est l'un des deux cours validés et la règle d'inscription s'applique. Une base de données en monde clos peut obtenir la même réponse en considérant comme faux les faits absents concernant les prérequis.

Choisir ce qui devient un objet

Une ontologie est le vocabulaire et les hypothèses structurelles qui l'accompagnent. Red(x) traite le rouge comme une propriété. Color(x, Red) fait de Red un objet, ce qui permet à ∃c (Color(x, c) ∧ Color(y, c)) d'exprimer une couleur commune. Cette opération est la réification : elle permet au langage de parler d'une propriété ou d'une catégorie comme d'une chose à part entière.

ASK peut demander si CanEnroll(Mia, AI) est une conséquence logique. ASKVARS peut demander les liaisons pour CanEnroll(x, AI), et renvoyer une substitution comme {x/Mia}. La même base permet de poser des questions de vérité et des requêtes pour trouver les objets correspondants.

Corriger le sens, pas seulement la syntaxe

Un axiome manquant peut empêcher d'obtenir une conséquence logique souhaitée ; un axiome incorrect peut en entraîner une indésirable. Teste des exemples positifs, des exemples négatifs et des cas limites. La règle ∀c (Course(c) ⇒ ∃t Teaches(t, c)) est trop forte si certains cours n'ont pas encore d'enseignant. La règle ∀p ∀c (Prereq(p, c) ⇒ Passed(Mia, p)) est trop forte parce qu'elle attribue à Mia la validation de tous les prérequis de tous les cours.

Les noms des prédicats sont des désignations pour le système de raisonnement. Nommer une relation Prereq ne fournit en soi aucune règle d'inscription. Les règles doivent relier les faits sur les prérequis, les cours validés et le droit à l'inscription dans le sens voulu.

L'inférence du premier ordre travaille sur des motifs contenant des variables. La substitution remplace des variables par des termes ; l'unification trouve des remplacements qui rendent deux expressions identiques. Ensemble, elles permettent à une règle générale de servir pour de nombreux faits particuliers sans engendrer d'abord toutes les instances possibles.

Instancier soigneusement les formules quantifiées

L'instanciation universelle remplace une variable liée universellement par n'importe quel terme clos. De ∀x (Cat(x) ⇒ Mammal(x)), déduis Cat(Tom) ⇒ Mammal(Tom), ou l'instance correspondante avec MotherOf(Tom). Un terme clos ne contient aucune variable.

L'instanciation existentielle introduit un nouveau nom de témoin. De ∃x (Crown(x) ∧ OnHead(x, John)), introduis une nouvelle constante C₁ et ajoute Crown(C₁) et OnHead(C₁, John). Nommer Ben comme témoin identifierait à tort un objet non précisé à un objet existant. La base de connaissances étendue préserve la satisfiabilité, pas l'équivalence dans le vocabulaire élargi.

La propositionnalisation engendre des instances closes, puis utilise le raisonnement propositionnel. Les symboles de fonction peuvent produire une infinité de termes : Ada, MotherOf(Ada), MotherOf(MotherOf(Ada)), et ainsi de suite. Les requêtes du premier ordre qui sont des conséquences logiques ont des preuves finies, mais un démonstrateur général peut s'exécuter indéfiniment lorsqu'une requête n'est pas une conséquence logique. C'est la semi-décidabilité.

Trouver une substitution cohérente

Pour unifier Knows(Ana, x) avec Knows(y, Bo), fais d'abord correspondre le prédicat et l'arité. Les premiers arguments imposent y = Ana ; les seconds imposent x = Bo. La substitution {y/Ana, x/Bo} transforme les deux expressions en Knows(Ana, Bo).

Knows(Ana, x) et Knows(y, MotherOf(y)) donnent quant à elles {y/Ana, x/MotherOf(Ana)}. Une liaison doit être propagée dans les autres termes. Si la même variable x apparaît dans les deux expressions Knows(Ana, x) et Knows(x, Bo), elle devrait devenir à la fois Ana et Bo : l'unification syntaxique échoue donc.

Les variables de formules quantifiées séparément sont indépendantes. Le renommage des variables les modifie avant de combiner les formules. Renommer le second x en z dans cette dernière paire permet d'obtenir {z/Ana, x/Bo}. Cela préserve l'indépendance voulue des variables locales des deux règles.

Un unificateur le plus général n'impose aucune liaison inutile. Knows(Ana, x) et Knows(y, z) s'unifient avec {y/Ana, x/z} ; attribuer aussi Ana à z spécialiserait inutilement le résultat. Le test d'occurrence rejette x = MotherOf(x), car un terme fini ne peut pas se contenir lui-même. L'unification ordinaire de Prolog peut autoriser des termes cycliques : son comportement demande donc de l'attention lorsque l'on veut utiliser une logique du premier ordre à termes finis.

Appliquer la règle mise en correspondance

Le modus ponens généralisé fait correspondre chaque prémisse avec une seule substitution cohérente. Owns(Ada, Atlas) et Book(Atlas) correspondent à Owns(x, y) ∧ Book(y) ⇒ Reader(x) avec {x/Ada, y/Atlas}, ce qui donne Reader(Ada). Faire correspondre une prémisse avec y = Atlas et une autre avec y = Beowulf ne justifierait pas le déclenchement de la règle : les variables partagées imposent les mêmes objets.

Une clause définie du premier ordre possède des prémisses atomiques et une conclusion atomique unique, ses variables étant implicitement quantifiées universellement. Les chaînages avant et arrière utilisent l'unification pour appliquer ces règles à des objets nommés. Datalog conserve cette forme de règle et exclut les symboles de fonction, ce qui donne un espace fini de faits clos possibles dans le cadre habituel d'une base de données finie.

Déduire les emplacements accessibles

Prends Link(A, B), Link(B, C) et Link(C, D). Utilise Link(x, y) ⇒ Reach(x, y), et Link(x, y) ∧ Reach(y, z) ⇒ Reach(x, z). Lors de tours synchrones, chaque règle utilise les faits disponibles avant le début du tour.

Le tour 1 déduit Reach(A, B), Reach(B, C) et Reach(C, D). Le tour 2 ajoute Reach(A, C) et Reach(B, D). Le tour 3 ajoute Reach(A, D). Le tour 4 n'ajoute rien. Il y a six faits Reach au point fixe. Une implémentation qui réutilise immédiatement les nouveaux faits peut les trouver dans un autre ordre, mais atteint la même clôture.

Avec n constantes et des prédicats d'arité au plus k, seul un nombre fini de tuples est possible ; une borne supérieure est p · nᵏ pour p prédicats. À l'inverse, NatNum(0) et NatNum(n) ⇒ NatNum(S(n)) engendrent des termes de profondeur toujours croissante, sans fin. Les symboles de fonction suppriment la garantie d'un domaine fini.

Faire correspondre une règle à plusieurs prémisses est un problème de contraintes. Une prémisse sélective peut réduire fortement le nombre de substitutions à examiner ensuite. Le chaînage avant incrémental se concentre sur les règles concernées par les faits nouvellement ajoutés. Les réseaux Rete conservent les correspondances partielles d'une mise à jour à l'autre, ce qui évite de répéter le travail dans les systèmes à règles de production.

Raisonner à rebours avec les liaisons

Pour démontrer Reach(A, D), essaie la règle du lien direct, qui exige le fait absent Link(A, D). La règle récursive exige quant à elle Link(A, y) et Reach(y, D). La première prémisse lie y à B. En poursuivant par B et C, on atteint le fait connu Link(C, D). La requête Reach(A, w) a trois réponses : w = B, C ou D.

Prolog écrit les règles avec la tête en premier et utilise des variables en majuscules et des constantes en minuscules :

reach(X, Y) :- link(X, Y).
reach(X, Z) :- link(X, Y), reach(Y, Z).

Il essaie les clauses de haut en bas et les prémisses de gauche à droite par chaînage arrière en profondeur. Le calcul peut utiliser N is M + 1. La négation par l'échec, notée \+ p, réussit si la tentative de démontrer p échoue en un temps fini. C'est un test opérationnel de l'échec, pas une preuve générale de la négation classique.

Éviter que la récursion ne piège la recherche

Placer reach(X, Y) en premier dans le corps récursif peut immédiatement rappeler le même but non résolu. Placer les clauses de base en premier et utiliser une récursion qui parcourt un lien aide, mais les cycles peuvent encore piéger les recherches infructueuses. La tabulation enregistre les réponses aux sous-buts et gère les dépendances répétées. Le chaînage avant est complet pour Datalog fini ; la recherche arrière naïve en profondeur a besoin de ce type de contrôle pour ne pas manquer des réponses accessibles derrière des branches infinies.

La résolution du premier ordre étend le raisonnement sur les clauses grâce à l'unification. Elle peut démontrer des conclusions portant sur des objets non nommés, car les termes de Skolem préservent les dépendances des témoins existentiels. Comme pour la réfutation propositionnelle, commence par la base de connaissances et la négation de la requête.

Préparer les clauses du premier ordre

Élimine ⇔ et ⇒, fais entrer les négations, renomme les variables liées, skolémise les variables existentielles, supprime les quantificateurs universels, puis distribue ∨ sur ∧. Il est important de faire entrer d'abord la négation, car ¬∀x P(x) devient ∃x ¬P(x), ce qui change le type de témoin nécessaire.

Pour « Chaque cours a un enseignant », ∀c (Course(c) ⇒ ∃t Teaches(t, c)), le témoin représentant l'enseignant peut dépendre de c. Introduis une nouvelle fonction T(c) pour obtenir ¬Course(c) ∨ Teaches(T(c), c). Une constante unique imposerait un seul enseignant pour tous les cours, ce que la formule initiale n'exige pas. Pour ∃t ∀c (Course(c) ⇒ Teaches(t, c)), une nouvelle constante convient, car le témoin précède le quantificateur universel.

« Tous les oiseaux ne volent pas » devient ∃x (Bird(x) ∧ ¬Flies(x)), puis Bird(B₁) et ¬Flies(B₁). Les deux clauses utilisent le même nouveau témoin. La skolémisation préserve la satisfiabilité ; elle ne donne pas une équivalence ordinaire sur le vocabulaire étendu.

Appliquer un unificateur à toute la clause résultante

Renomme les variables des deux clauses pour les distinguer. Trouve des littéraux complémentaires qui s'unifient, supprime-les et applique leur unificateur le plus général à chaque littéral restant. La factorisation fusionne aussi les littéraux d'une clause qui peuvent être unifiés. La résolution avec factorisation est complète pour la réfutation des clauses du premier ordre.

Prends ¬Course(c) ∨ Teaches(T(c), c), ¬Teaches(u, v) ∨ Staff(u), et Course(Logic). La requête est ∃w Staff(w) ; sa négation donne ¬Staff(w), quantifiée universellement. Applique la résolution au fait concernant le cours et à la première clause pour obtenir Teaches(T(Logic), Logic). Applique la résolution avec la deuxième clause sous {u/T(Logic), v/Logic}, ce qui donne Staff(T(Logic)). Applique la résolution avec ¬Staff(w) sous {w/T(Logic)} pour obtenir la clause vide. Un membre du personnel existe, même si la base de connaissances ne donne jamais à cette personne un nom ordinaire.

Contrôler la recherche parmi les clauses

La préférence unitaire choisit d'abord les clauses courtes. La stratégie de l'ensemble de support exige qu'une clause parente provienne de la négation de la requête ou en soit déduite ; elle préserve la complétude lorsque le reste de la base de connaissances est satisfiable. La résolution par entrée exige une clause parente initiale à chaque étape et est complète pour les bases de clauses de Horn. La subsomption supprime une clause plus faible déjà couverte par une clause générale plus forte, par exemple P(Ana) ∨ Q(Bo) lorsque P(x) est connue.

L'égalité nécessite un traitement particulier : des axiomes d'égalité, la réécriture par des équations au moyen de la démodulation ou des inférences comme la paramodulation. La seule résolution purement syntaxique ne rend pas compte de tous les aspects de l'égalité. Une recherche complète et équitable trouve une contradiction pour tout ensemble insatisfiable de clauses du premier ordre, mais peut s'exécuter indéfiniment dans le cas contraire. Parmi les démonstrateurs fondés sur la résolution figurent Vampire et E ; EQP a démontré la conjecture de Robbins en 1996.

Une ontologie organise les catégories, les objets, les relations et les hypothèses d'un domaine. Une ontologie de haut niveau fournit des notions générales comme les objets, les événements et le temps ; une ontologie de domaine fournit les distinctions utiles dans un domaine particulier. Les ontologies cliniques et biologiques illustrent pourquoi un vocabulaire commun utile sert souvent une communauté précise.

Distinguer l'appartenance et la relation de sous-classe

Une catégorie peut apparaître comme un prédicat, Laptop(x), ou comme un objet, Laptops. L'appartenance x ∈ Laptops dit qu'un individu en est membre. Laptops ⊂ Computers dit que tout ordinateur portable est un ordinateur. Une taxonomie organise ces relations de sous-classe en hiérarchie. Si tout ordinateur a un processeur, les ordinateurs portables héritent de cette propriété.

La relation de sous-classe est transitive : Penguins ⊂ Birds et Birds ⊂ Animals donnent Penguins ⊂ Animals. L'appartenance n'est pas transitive. Pingu ∈ Penguins et Penguins ∈ Species ne font pas de Pingu une espèce. Un énoncé concerne un oiseau individuel ; l'autre concerne une catégorie traitée comme un objet.

Des catégories sont disjointes si elles n'ont aucun membre commun. Une décomposition exhaustive couvre chaque membre de la catégorie parente. Une partition vérifie les deux conditions : les entiers négatifs, zéro et les entiers positifs forment une partition des entiers. L'exhaustivité permet des recouvrements, sauf si la disjonction est également énoncée.

Représenter les parties, les événements et les valeurs héritées

PartOf décrit la composition, pas l'appartenance à une catégorie. PartOf est transitif : un rayon appartenant à une roue qui appartient à un vélo fait partie du vélo. Un vélo n'est pas pour autant une sorte de roue. Les événements peuvent aussi être des objets : Happens(e, t), Initiates(e, f, t) et HoldsAt(f, t) relient les événements aux fluents qui changent. Allumer une lampe initialise un fluent qui persiste jusqu'à ce qu'un événement y mette fin.

Un réseau sémantique représente les objets et les catégories par des nœuds reliés par des relations étiquetées. Dans un réseau avec des valeurs par défaut, « les oiseaux volent normalement » peut fournir une valeur héritée par les oiseaux ordinaires, tandis qu'une catégorie plus spécifique de manchots la remplace. Cela diffère de l'affirmation de l'axiome classique sans exception ∀x (Bird(x) ⇒ Flies(x)), qui s'appliquerait aussi aux manchots.

Choisir le langage de raisonnement

Les logiques de description permettent la subsomption, la classification et la vérification de cohérence. Une définition peut classer une personne ayant au moins trois enfants dans une catégorie appropriée. Ces logiques servent de fondement aux langages de logique de description d'OWL.

Le raisonnement par défaut est non monotone : apprendre qu'un oiseau est un manchot peut retirer la conclusion selon laquelle il vole, obtenue par défaut. La circonscription minimise les cas anormaux dans des règles comme Bird(x) ∧ ¬Abnormal(x) ⇒ Flies(x). La logique des défauts permet de tirer des conclusions tant qu'elles restent cohérentes avec les connaissances. Les systèmes de maintien de la vérité enregistrent les justifications afin de pouvoir retirer les conclusions qui dépendent d'une croyance abandonnée.

Un graphe de connaissances stocke des entités et leurs relations sous forme de graphe orienté. Un arc simple devient un triplet : sujet, prédicat, objet. Par exemple, (Ada, worksAt, Lab) correspond à WorksAt(Ada, Lab) ; (Ada, type, Researcher) énonce une appartenance à une catégorie. Un schéma donne un sens commun à ces désignations et permet d'autres inférences.

Distinguer les standards du Web

RDF représente les graphes sous forme de triplets. Les sujets sont des IRI ou des nœuds anonymes, les prédicats sont des IRI et les objets peuvent aussi être des valeurs littérales. Les IRI identifient les ressources d'un jeu de données à l'autre ; un nœud anonyme représente une ressource sans lui donner d'identifiant global. RDFS ajoute des classes, des relations de sous-classe ainsi que le domaine et l'ensemble des valeurs des propriétés. OWL fournit des définitions d'ontologie plus riches. SPARQL recherche des correspondances avec des motifs de graphe pour renvoyer des liaisons de variables. Les graphes de propriétés offrent un autre modèle avec des propriétés clé-valeur sur les nœuds et les arcs ; Cypher et GQL sont des langages de requête pour cette famille.

Si Ada est de type Researcher et que Researcher est une sous-classe de Scientist, une règle de sous-classe permet de déduire qu'Ada est de type Scientist. Il s'agit d'un chaînage avant du premier ordre sur Member(x, c) ∧ Subset(c, d) ⇒ Member(x, d). Pour rendre ce fait déduit accessible, un moteur de requêtes sur graphe doit prendre en charge la conséquence logique correspondante ou disposer des conclusions matérialisées.

Faire correspondre une requête et préserver les détails

Avec ex: déclaré comme préfixe d'IRI, une requête peut être :

SELECT ?p WHERE {
  ?p a ex:Researcher .
  ?p ex:worksAt ex:Lab .
}

Le même ?p doit satisfaire les deux motifs. Il s'agit d'une jointure, pas de deux recherches sans rapport. Les résultats sont des liaisons comme ?p = ex:Ada, semblables aux substitutions dans les requêtes logiques.

Un arc binaire ne peut pas à lui seul exprimer tous les rôles dans un événement daté. Pour un prix, crée un nœud d'événement ou d'énoncé et relie-le au destinataire, au prix et à l'année. Cela regroupe les détails d'une même attribution et évite d'attacher par erreur la date à tous les prix de ce type. Wikidata prend en charge des qualificatifs d'énoncé pour ces détails.

Distinguer les liens absents, déduits et prédits

RDF et OWL utilisent une lecture en monde ouvert : un arc absent concernant le conjoint laisse la relation inconnue. Les applications en monde clos font un autre choix pour les faits manquants. Un résultat de requête vide indique l'absence de correspondance dans les conditions de cette requête ; il n'établit pas à lui seul un fait négatif universel.

Wikidata, DBpedia, le Knowledge Graph de Google et les graphes internes des organisations permettent de répondre à des requêtes factuelles, de relier des enregistrements, de formuler des recommandations et de retrouver des informations pour les systèmes génératifs. Leurs faits peuvent être incomplets ou dépassés. La résolution d'entités identifie les enregistrements qui désignent la même chose même lorsque leurs identifiants diffèrent.

Les plongements attribuent des vecteurs aux entités et aux relations. Dans TransE, l'apprentissage rapproche la somme du vecteur de tête et du vecteur de relation du vecteur de queue. Un score élevé suggère un lien manquant ; c'est une prédiction statistique. L'inférence logique déduit une conséquence de faits et de règles énoncés. Garde cette différence à l'esprit lorsque tu décides si un nouvel arc doit figurer parmi les faits vérifiés.

La planification classique recherche des actions qui mènent d'un état initial connu à un but. Le modèle est totalement observable, déterministe, discret et comporte un seul agent ; le monde change par les actions modélisées. Une représentation factorisée décrit chaque état à l'aide de fluents, de sorte qu'un planificateur peut raisonner sur ce que chaque action modifie.

Écrire l'état et les schémas d'action

Dans le fragment de base de PDDL de type STRIPS, un état énumère les fluents atomiques clos qui sont vrais. Les fluents non indiqués sont faux selon l'hypothèse du monde clos. Le domaine réutilisable déclare les prédicats et les schémas d'action ; le problème déclare les objets, l'état initial et un but. PDDL a été introduit pour la compétition de planification de 1998, en s'appuyant sur STRIPS.

Un schéma d'action possède des paramètres, une précondition et des effets. Go(r, from, to) exige At(r, from) et Connected(from, to) ; il ajoute At(r, to) et supprime At(r, from). Pick(r, p, l) exige At(r, l), In(p, l) et HandEmpty(r) ; il ajoute Holding(r, p) et supprime In(p, l) et HandEmpty(r). Drop exige la présence à l'emplacement et la possession du colis ; il ajoute l'emplacement du colis et le fait que la main est libre, et supprime le fait que le colis est tenu.

Une action close ne s'applique que lorsque ses préconditions sont vraies. Sa mise à jour est RESULT(s, a) = (s − DEL(a)) ∪ ADD(a). Les autres fluents persistent, y compris les faits statiques Connected. Cette persistance implicite traite le problème du cadre sans axiome distinct pour chaque fluent inchangé.

Suivre une livraison en quatre actions

Au départ, R est à Dock, Box est à Shelf et la main de R est libre. Des liens Connected relient Dock à Shelf et Shelf à Packing dans les deux sens. Le but est In(Box, Packing).

1. Go(R, Dock, Shelf) change l'emplacement de R et préserve les faits concernant la boîte et la main.
2. Pick(R, Box, Shelf) retire la boîte de l'étagère et la fait tenir par R.
3. Go(R, Shelf, Packing) déplace R tout en préservant Holding(R, Box).
4. Drop(R, Box, Packing) place la boîte à Packing et libère la main.

Le but ne précise pas l'emplacement final du robot, sauf dans la mesure où les actions l'exigent. Les buts décrivent généralement de nombreux états acceptables, pas un seul état complet.

Lire et vérifier un schéma

(:action pick
 :parameters (?r ?p ?l)
 :precondition (and (at ?r ?l) (in ?p ?l) (hand-empty ?r))
 :effect (and (holding ?r ?p)
              (not (in ?p ?l)) (not (hand-empty ?r))))

Omettre un effet de suppression peut laisser un robot à deux endroits ou un colis à la fois tenu et sur une étagère. Placer une condition nécessaire uniquement dans un effet conduit l'action à la créer au lieu de la vérifier.

Dans le monde des blocs, déplacer un bloc libre b de x sur un bloc libre y exige On(b, x), Clear(b), Clear(y), Block(b), Block(y) et ¬(b = y). L'action ajoute On(b, y) et Clear(x), et supprime On(b, x) et Clear(y). Les vérifications de distinction et de type bloc empêchent de placer un bloc sur lui-même et de traiter la table comme un seul bloc. Une action distincte MoveToTable garde la table disponible pour les autres blocs.

Un modèle de planification définit un espace de recherche, mais le choix d'actions utiles reste difficile. La progression recherche vers l'avant parmi des états complets. La régression de buts recherche vers l'arrière parmi les conditions qu'un état précédent doit satisfaire. Les deux peuvent réutiliser des méthodes générales de recherche tout en exploitant la structure des actions.

Rechercher depuis l'une ou l'autre extrémité

La progression part de l'état initial et applique les actions closes applicables. Elle peut gaspiller des efforts sur des actions non pertinentes : un robot, 20 boîtes et 10 emplacements donnent déjà 200 combinaisons Pick closes possibles avant le filtrage selon leur applicabilité.

La régression considère une action qui réalise un littéral du but sans en nier un autre. Effectue la régression d'un ensemble de buts g à travers a en retirant les littéraux réalisés et en ajoutant les préconditions : g′ = (g − EFFECT(a)) ∪ PRECOND(a). EFFECT contient les littéraux positifs et négatifs avec leur signe. Rejette tout résultat incohérent contenant un littéral et sa négation.

Pour In(Box, Packing) ∧ At(R, Dock), la régression à travers Drop(R, Box, Packing) donne Holding(R, Box) ∧ At(R, Packing) ∧ At(R, Dock). Ces conditions entrent en conflit avec l'invariant voulu selon lequel le robot n'occupe qu'un emplacement. Un plan valide doit livrer la boîte avant le retour final du robot. La régression à travers Go(R, Shelf, Dock) donne en revanche In(Box, Packing) ∧ At(R, Shelf) ∧ Connected(Shelf, Dock), ce qui préserve le fait que le colis est livré.

Estimer la distance avec des problèmes plus simples

Une heuristique est admissible lorsqu'elle ne surestime jamais le coût restant optimal. A* avec une heuristique admissible trouve un plan optimal. Compter les buts non satisfaits n'est pas toujours admissible : une seule action peut en réaliser plusieurs.

Ignorer les préconditions rend toutes les actions immédiatement utilisables. Ignorer les effets de suppression rend les progrès permanents, pour les problèmes exprimés avec des préconditions et des buts positifs. Les conditions négatives doivent d'abord être transformées en fluents positifs maintenus explicitement. La longueur optimale d'un plan relaxé h⁺ est un minorant de la longueur réelle du plan, mais son calcul est NP-difficile. FF trouve rapidement un plan relaxé sans garantir son optimalité ; sa longueur peut surestimer h⁺ et n'est pas nécessairement admissible.

Pour le but de livraison et de retour à l'entrepôt, le plan réel le plus court comporte six actions : aller à Shelf, prendre la boîte, aller à Packing, la déposer, revenir à Shelf, puis à Dock. La relaxation des effets négatifs ne nécessite que les quatre premières, car At(R, Dock) reste vrai après le départ. Ainsi h⁺ = 4 alors que le coût réel est de 6. Le nombre de buts non satisfaits n'est au départ que de 1 et ne rend pas compte de l'essentiel de ce travail.

Combiner les estimations sans compter deux fois

Un graphe de planification alterne des niveaux de fluents possibles et d'actions possibles, avec des liens d'exclusion mutuelle qui marquent les paires incompatibles. La première apparition d'un but donne une estimation en nombre de niveaux. Prendre le maximum des niveaux individuels des buts est admissible ; les additionner peut compter plusieurs fois un travail partagé. L'abstraction d'état retire certains fluents pour réduire l'espace d'états. Pour la décomposition en sous-buts aussi, il est utile de repérer les actions partagées : le maximum des coûts admissibles des sous-buts est admissible, tandis que leur somme nécessite une justification supplémentaire.

Les méthodes de planification diffèrent par ce sur quoi porte leur recherche : états, affectations de valeurs de vérité, contraintes d'ordre ou décompositions de procédures expertes. Leur utilité dépend de l'interaction des sous-buts et des hypothèses du modèle sur l'exécution.

Reconnaître les interactions entre sous-buts

Dans l'anomalie de Sussman, C est sur A, et A et B sont sur la table. Le but est On(A, B) ∧ On(B, C). Réaliser d'abord le sous-but qui place A sur B empêche ensuite de placer B. Placer immédiatement B sur C laisse A enfoui. Un plan de longueur minimale libère d'abord A, puis construit la pile par le bas : déplacer C sur la table, déplacer B sur C, puis déplacer A sur B. Les trois déplacements entrelacent la préparation et la réalisation des buts.

Encoder un plan borné comme problème SAT

SATPlan choisit un horizon T. Il énonce les fluents initiaux à l'instant 0, les fluents du but à T, les préconditions des actions, les contraintes d'état successeur et les exclusions pour les actions incompatibles. Une affectation satisfaisante sélectionne des actions qui forment un plan. Un résultat insatisfiable exclut les plans dans cet encodage et à cet horizon.

Essayer les horizons dans l'ordre permet de trouver le plus petit horizon satisfiable. Avec des actions parallèles, cela minimise les couches, pas nécessairement le nombre total d'actions. Une borne d'arrêt est nécessaire pour conclure à l'absence de plan à partir d'une succession d'horizons insatisfiables.

Ne garder que l'ordre nécessaire

La planification à ordre partiel enregistre les actions, les contraintes d'ordre et les liens causaux. Un lien A - p → B dit que A établit la précondition p de B. Une action C qui pourrait supprimer p entre les deux est une menace. La rétrogradation place C avant A ; la promotion la place après B. Les actions sans rapport peuvent rester sans ordre fixé jusqu'à l'exécution, selon le principe d'engagement minimal.

La planification par réseaux de tâches hiérarchiques décompose les tâches de haut niveau à l'aide d'une bibliothèque de méthodes. DeliverBox peut devenir : aller jusqu'à la boîte, la prendre, aller à destination et la déposer. Ces méthodes encodent des procédures expertes ; la recherche peut donc se concentrer sur des décompositions utiles au lieu de considérer chaque action élémentaire à chaque étape.

Adapter le modèle au monde

L'existence d'un plan pour STRIPS propositionnel général est PSPACE-complète. Dans le monde des blocs, le problème d'existence est plus facile pour les dispositions possibles : déplacer les blocs sur la table et reconstruire, en utilisant au plus 2n déplacements pour n blocs. Trouver un plan de longueur minimale pour le monde des blocs reste NP-difficile.

Les modèles classiques ne prennent pas en compte les résultats incertains, l'état caché et les durées des actions. Les plans sans capteurs fonctionnent sans observations, les plans contingents comportent des branches selon les observations, la replanification en ligne réagit aux écarts pendant l'exécution et l'ordonnancement gère les temps et les ressources. Une précondition de batterie manquante peut faire échouer physiquement un plan valide dans le modèle. La surveillance de l'exécution permet de vérifier cet écart. La planification automatique a été utilisée dans des systèmes réels, notamment Remote Agent de la NASA sur Deep Space 1 en 1999.