🤖 AI

Hybrid MKNF with Classical Negation in the Rule Component

Cet article introduit une extension des bases de connaissances MKNF hybrides qui incorpore la négation classique dans la composante de règle afin de mieux prendre en charge le raisonnement négatif explicite dans les applications critiques pour la sécurité, en fournissant des définitions formelles et une procédure pour calculer le modèle bien fondé.

Auteurs originaux : Arun Raveendran Nair Sheela, Christophe Rey, Florence De Grancey

Publié 2026-07-24

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Arun Raveendran Nair Sheela, Christophe Rey, Florence De Grancey

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de construire un robot super intelligent capable de comprendre le monde. Pour ce faire, vous devez lui enseigner deux manières de penser très différentes. La première est celle d'un bibliothécaire strict qui connaît chaque fait d'une encyclopédie massive ; si le livre ne dit pas qu'un dragon existe, le bibliothécaire suppose qu'il n'existe pas, mais il est prudent de ne déclarer que ce qui est explicitement écrit. La seconde est celle d'un détective qui résout des mystères en cherchant des indices ; si le détective ne trouve aucune preuve concernant un suspect, il peut supposer que le suspect est innocent, mais seulement jusqu'à l'apparition de nouvelles preuves.

Pendant des années, des scientifiques ont tenté de combiner ces deux penseurs en un seul cerveau. Ce domaine est appelé « Représentation des Connaissances » (Knowledge Representation), et c'est l'épine dorsale de la manière dont les ordinateurs raisonnent sur des choses complexes, allant du diagnostic médical aux voitures autonomes. La méthode spécifique que cet article examine est appelée « MKNF hybride ». Considérez cela comme un mariage entre l'encyclopédie du bibliothécaire (appelée Logiques de Description) et le carnet de règles du détective (appelée Programmation Logique). L'objectif est de permettre à l'ordinateur d'utiliser l'encyclopédie pour comprendre la structure du monde tout en utilisant le carnet de règles pour gérer les situations changeantes, comme le trafic ou la météo. Cependant, il y a un piège : le carnet de règles du détective a un angle mort. Il peut dire « Je ne sais pas s'il pleut » (parce qu'il n'y a pas de rapport), mais il a du mal à dire « Je sais avec certitude qu'il ne pleut pas » (parce qu'il y a un rapport indiquant que le ciel est dégagé). C'est un problème majeur pour les systèmes critiques pour la sécurité, comme les pistes d'aéroport, où savoir que quelque chose n'est absolument pas cassé est aussi important que de savoir qu'il est cassé.

Cet article introduit une nouvelle mise à niveau pour ce carnet de règles de détective, permettant de gérer la « négation classique » — la capacité d'énoncer explicitement que quelque chose est faux, plutôt que de simplement supposer que c'est faux parce que l'information est manquante. Les auteurs, Sheela, Rey et De Grancey, proposent un nouveau système appelé hMKNF¬. Ils n'ont pas seulement suggéré cette idée ; ils ont construit un cadre mathématique complet pour prouver qu'elle fonctionne. Ils ont montré comment définir les règles de ce nouveau système et ont créé une recette étape par étape (un algorithme) pour que l'ordinateur trouve la « meilleure » réponse, connue sous le nom de « modèle bien fondé » (well-founded model). Ils ont prouvé que cette nouvelle méthode peut gérer n'importe quel mélange de faits et de règles, même lorsqu'ils deviennent complexes, et ils ont fourni un moyen de calculer la réponse en trois phases distinctes, garantissant que le robot ne soit jamais confus par une information manquante ou des indices contradictoires.

Le nouveau super-pouvoir du détective

Imaginez que vous gériez un aéroport très fréquenté. Vous avez une immense base de données (l'Ontologie) qui répertorie chaque piste, chaque aéroport et chaque avion. Cette base de données est le « Bibliothécaire ». Elle sait que la Piste 4 se trouve à l'Aéroport X. Mais la base de données ne connaît pas la météo actuelle. C'est là que le « Détective » intervient. Le Détective utilise un ensemble de règles pour décider si une piste est sûre à utiliser.

Dans l'ancien système, la règle du Détective pour une piste sûre ressemblait à ceci : « Si la piste se trouve dans un aéroport, et que nous ne savons pas qu'elle est fermée, et que nous ne savons pas s'il y a un obstacle, alors la piste est ouverte. »

Voici le problème : Et si le rapport météo est retardé ? Le Détective ne sait pas s'il y a un obstacle. Dans l'ancien système, parce que le Détective ne trouve pas de rapport d'obstacle, il pourrait supposer qu'il n'y en a pas et dire : « La piste est ouverte ! ». Mais et si un énorme rocher se trouvait sur la piste, et que le rapport n'est simplement pas encore arrivé ? L'ancien système commettrait une erreur dangereuse car il traite « l'information manquante » comme une « preuve d'absence ».

L'article soutient que dans les situations critiques pour la sécurité, nous avons besoin que le Détective soit capable de dire : « J'ai vérifié, et je sais qu'il n'y a pas d'obstacle. » C'est ce qu'on appelle la « négation classique ». C'est la différence entre dire « Je n'ai pas vu de fantôme » et dire « J'ai vérifié qu'il n'y a pas de fantômes ».

Le flux de travail en trois phases du détective

Les auteurs ont réalisé que l'ajout de ce pouvoir de « savoir que c'est faux » rend les mathématiques beaucoup plus difficiles. On ne peut pas simplement deviner la réponse ; il faut en être sûr. Ils ont donc conçu un processus en trois phases pour résoudre ces énigmes, comme un détective travaillant sur une affaire avec des niveaux de surveillance croissants.

Phase 1 : Le scan rapide (Calcul du point fixe)
D'abord, le système effectue un scan automatique rapide. Il examine toutes les règles et tous les faits et demande : « Que pouvons- nous prouver avec certitude dès maintenant ? ». Il construit une liste de choses qui sont définitivement vraies et de choses qui sont définitivement fausses. Si l'énigme est simple, cette phase la résout instantanément. Le système utilise un « opérateur bien fondé », qui est comme une machine qui ajoute sans cesse de nouveaux faits jusqu'à ce qu'elle ne puisse plus en ajouter. Si la machine s'arrête et que la réponse est cohérente, nous avons terminé !

Phase 2 : La chaîne logique (Propagation d'unité)
Parfois, le Scan Rapide reste bloqué. Il trouve une règle qui dit : « Si A est vrai, alors B est faux », mais il ne sait pas encore si A est vrai. Cependant, il peut savoir que si A était vrai, cela briserait une règle. Ainsi, le système force une décision. Il dit : « D'accord, si le fait que A soit vrai provoque une contradiction, alors A doit être faux. » C'est ce qu'on appelle la « Propagation d'unité » (Unit Propagation). C'est comme un détective réalisant : « Si le majordome l'a fait, l'horloge serait cassée. L'horloge n'est pas cassée, donc le majordome ne l'a pas fait. » Cette phase force le système à faire des déductions logiques que la première phase a manquées.

Phase 3 : Le devine-et-vérifie (Le dernier recours)
Parfois, même après le Scan Rapide et la Chaîne Logique, le système est toujours bloqué. Il y a trop de possibilités et les règles sont trop emmêlées. C'est là que les auteurs admettent que, parfois, il faut simplement deviner. Ils proposent une phase de « Devine-et-Vérifie » (Guess-and-Check). Le système essaie toutes les combinaisons possibles de « Vrai » et de « Faux » pour les inconnues restantes. Il vérifie chaque supposition pour voir si elle crée une histoire stable et cohérente. S'il trouve une histoire qui fonctionne et qui est la plus « sûre » (c'est-à-dire qu'elle laisse le moins de choses indéfinies), alors c'est la réponse. L'article note que cette phase est la plus coûteuse en termes de calcul — c'est comme essayer chaque clé d'un immense trousseau — mais elle est nécessaire pour s'assurer que le système ne manque jamais une solution valide.

Pourquoi cela importe

Les auteurs n'ont pas seulement inventé un nouveau jeu ; ils ont construit une preuve mathématique rigoureuse que ce nouveau système fonctionne. Ils ont montré que leur méthode, hMKNF¬, peut gérer n'importe quel mélange de faits et de règles, même les plus désordonnés, là où les choses pourraient se contredire. Ils ont prouvé que leur processus en trois phases trouvera toujours le « modèle bien fondé » — la réponse la plus fiable et la moins risquée possible.

Ils ont également comparé leur méthode aux tentatives précédentes. Les anciennes méthodes ne pouvaient gérer que des cas simples ou exigeaient que les règles soient très spécifiques (comme ne traiter que des éléments isolés, et non des groupes complexes). Leur nouvelle méthode est plus flexible et plus puissante. Cependant, ils sont honnêtes quant au compromis : parce qu'ils autorisent ce pouvoir supplémentaire (la négation classique), la phase de « Devine-et-Vérifie » peut prendre du temps pour des problèmes très complexes. Mais pour les applications critiques pour la sécurité, comme s'assurer qu'un avion ne décolle pas d'une piste bloquée, prendre un peu plus de temps pour être sûr à 100 % est un prix qui vaut la peine d'être payé.

En résumé, cet article donne aux ordinateurs un nouveau super-pouvoir : la capacité de savoir explicitement ce qui n'est pas vrai, et pas seulement ce qui est manquant. En combinant un scan rapide, une chaîne logique et un examen minutieux de type devine-et-vérifie, ils ont construit un système capable de raisonner sur le monde avec une précision et une sécurité bien plus grandes.

Résumé technique : hMKNF¬ avec négation classique dans la composante de règles

Énoncé du problème
Les bases de connaissances hybrides MKNF intègrent les logiques de description (DL) avec la programmation logique pour soutenir le raisonnement en monde ouvert et en monde fermé. Bien que la sémantique de fondement (well-founded semantics) pour le MKNF hybride, telle qu'établie dans les travaux antérieurs [5], permette un calcul efficace en temps polynomial du modèle de fondement, elle manque de support pour la négation classique au sein de la composante de règles. Dans le cadre existant, l'information négative est exprimée uniquement par la négation par défaut (not), où l'absence de dérivation implique la négation d'un fait. Cette limitation est critique dans les domaines de sécurité critique où une connaissance négative explicite est requise ; se fier à l'absence d'information peut conduire à des inférences dangereuses (par exemple, supposer qu'une piste est dégagée simplement parce qu'aucun obstacle n'a été signalé). De plus, les transformations syntaxiques existantes pour simuler la négation classique sont restreintes aux prédicats unaires et nécessitent une ingénierie de la connaissance supplémentaire. En outre, les méthodes de calcul par le bas (bottom-up) précédentes [5] ne garantissent de produire le modèle de fondement correct que pour les bases MKNF hybrides cohérentes ; pour les bases non cohérentes, elles peuvent produire des modèles différents de la sémantique déclarative [7].

Méthodologie
Les auteurs introduisent hMKNF¬, une extension du MKNF hybride qui permet une négation classique sans restriction dans la composante de règles tout en maintenant la sécurité DL (DL-safety) pour garantir la décidabilité. La méthodologie procède par les étapes suivantes :

Définition formelle : La syntaxe de hMKNF¬ autorise des règles de la forme $K H \leftarrow b^+(r), b^-(r)$ , où $b^-(r)$ contient des atomes de la forme not $\xi$ , $\xi$ étant soit un atome $A$ , soit sa négation classique $\neg A$ . Les sémantiques sont définies via une structure MKNF à trois valeurs $(I, M, N)$ , où l'évaluation des atomes modaux classiquement niés (par exemple, $K\neg \phi$ et not $\neg \phi$ ) est adaptée des sémantiques MKNF standards.
Caractérisation à trois valeurs : Le papier adapte le concept de partitions stables de [7] à hMKNF¬. Une partition partielle $(T, F)$ de l'ensemble des atomes modaux instanciés est définie, où $T$ représente les atomes vrais et $F$ représente les atomes faux. Le modèle de fondement est caractérisé comme l'unique partition stable minimale.
Procédure de calcul : Une procédure opérationnelle en trois phases est proposée pour calculer la partition de fondement :
- Phase 1 (Opérateur de fondement) : Un calcul de point fixe itératif utilisant un opérateur de fondement $W_{KG}$ , qui combine un opérateur de dérivation ( $T^F_{KG}$ ) et un opérateur d'ensemble infondé ( $F_{KG}$ ). Cette phase calcule une partition partielle $(T_\omega, F_\omega)$ .
- Phase 2 (Propagation d'unité) : Si la Phase 1 ne produit pas une partition stable, un opérateur de propagation d'unité $E_{KG}$ est appliqué. Cette phase gère les cas où la tête d'une règle est fausse et son corps est indéfini, forçant la valeur de vérité de certains atomes pour satisfaire la règle. Cela résulte en une partition raffinée $(T_E, F_E)$ .
- Phase 3 (Devine et vérifie / Guess-and-Check) : Si la partition n'est toujours pas stable, la procédure énumère toutes les extensions de la partition actuelle sur les atomes indéfinis restants. Elle vérifie chaque candidat par rapport aux conditions de stabilité (Prop. 3.2) pour identifier toutes les partitions stables et sélectionne la minimale (la partition de fondement).

Contributions clés
Le papier apporte trois contributions primaires :

Formalisme hMKNF¬ : L'introduction de hMKNF¬, une extension du MKNF hybride qui supporte formellement la négation classique dans la composante de règles, répondant aux limitations de la négation par défaut pour représenter la connaissance négative explicite.
Sémantique à trois valeurs : Une caractérisation formelle des bases de connaissances hMKNF¬ via des partitions stables, établissant que le modèle de fondement correspond à l'unique partition stable minimale.
Procédure de calcul : Un algorithme général en trois phases pour calculer le modèle de fondement de bases de connaissances hMKNF¬ arbitraires. Cette procédure gère à la fois les bases de connaissances cohérentes et non cohérentes et intègre le raisonnement DL avec des règles de programmation logique contenant la négation classique.

Résultats et Complexité
Le papier établit la correction théorique de la procédure proposée.

Correction : Le Théorème 4.1 prouve que la sortie de l'algorithme en trois phases identifie correctement la partition de fondement si elle existe, détecte l'incohérence MKNF (retourne $\bot$ ), ou identifie l'absence d'un modèle de fondement unique (retourne NoWFM).
Complexité : La complexité des données dépend de la phase dans laquelle la partition stable est trouvée.
- Si elle est trouvée en Phase 1 ou 2, la complexité est polynomiale par rapport à la complexité des données du raisonnement DL et du calcul de l'ensemble infondé ( $PTime^{C_1 \cup C_2}$ ).
- Si elle n'est trouvée qu'en Phase 3, la complexité est exponentielle ( $EXPTime^{P^{C_1}}$ ) en raison de l'énumération des candidats, bien que les vérifications de stabilité individuelles restent polynomiales par rapport au raisonnement DL.
Comparaison : Contrairement à l'approche de [5], qui est limitée aux bases de connaissances cohérentes et manque de la négation classique, hMKNF¬ s'applique à toutes les bases de connaissances MKNF hybrides et supporte la négation classique. Contrairement à la méthode générale de "guess-and-check" de [7], hMKNF¬ privilégie le calcul déterministe via les Phases 1 et 2, ne recourant au "guessing" non déterministe que lorsque cela est nécessaire.

Signification
Le papier affirme que hMKNF¬ comble une lacune importante dans la représentation des connaissances hybrides en permettant la représentation explicite de l'information négative au sein de la composante de règles. Cela est particulièrement significatif pour les applications de sécurité critique où le raisonnement doit s'appuyer sur une preuve explicite d'absence plutôt que sur la simple absence d'information positive. En fournissant une procédure générale qui fonctionne pour les bases de connaissances cohérentes et non cohérentes, ce travail étend l'applicabilité du MKNF hybride à des scénarios plus complexes et réalistes. Les auteurs notent que bien que la phase de "guess-and-check" introduise une complexité exponentielle dans le pire des cas, celle-ci est inévitable pour assurer la correction et l'exhaustivité du modèle de fondement pour les bases de connaissances hMKNF¬ arbitraires. Ce travail pose les bases de futurs systèmes de réponse aux requêtes basés sur ce formalisme étendu.

Le nouveau super-pouvoir du détective

Le flux de travail en trois phases du détective

Pourquoi cela importe

Articles similaires