💻 computer science

Obligation-Producing Actions

Cet article présente une solution simplifiée au problème du cadre pour les actions produisant des obligations en étendant les théories d'actions de base de Reiter et l'opérateur de régression pour modéliser la manière dont de telles actions génèrent des obligations persistantes sans recourir à la notion de situations idéales.

Auteurs originaux : Kalonji Kalala, Iluju Kiringa, Tet Yeap

Publié 2026-06-16

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Kalonji Kalala, Iluju Kiringa, Tet Yeap

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 jouez à un jeu de société complexe où les règles ne consistent pas seulement à déplacer des pièces, mais à créer des promesses qui doivent être tenues. Ce document traite de la création d'un livre de règles parfait pour qu'un ordinateur puisse comprendre ces promesses, les suivre au fur et à mesure que le jeu évolue, et déterminer la suite sans s'embrouiller.

Voici la décomposition des idées de ce document en utilisant des analogies simples :

1. Le Problème : L'énigme du « Qu'est-ce qui reste identique ? »

Dans le monde de l'IA, il existe un casse-tête célèbre appelé le problème du cadre (Frame Problem). Imaginez que vous êtes dans une pièce. Si vous allumez la lumière, la lumière s'allume. Mais est-ce que la couleur des murs a changé ? Est-ce que le chat sur le canapé a soudainement appris à voler ? Est-ce que le solde de votre compte bancaire a changé ?

Dans la vie réelle, nous savons que 99 % des choses ne changent pas lorsqu'on fait une petite action. Mais pour un ordinateur, lister chaque chose qui ne change pas est impossible. C'est comme essayer d'écrire une règle pour un jeu vidéo qui dirait : « Quand tu sautes, tu montes, mais le ciel reste bleu, l'herbe reste verte, la lune reste lointaine et tes lacets restent noués... » Cela prendrait une éternité.

Les auteurs du document sont des experts pour résoudre cette énigme pour les actions normales (comme ouvrir une porte). Maintenant, ils résolvent cela pour les promesses (obligations).

2. Le Nouveau Défi : Les « Actions Produisant des Obligations »

Les auteurs introduisent un type spécial de mouvement dans le jeu appelé une Action Produisant une Obligation.

L'Analogie :
Imaginez que vous êtes la seule personne dans une maison. Vous décidez d'ouvrir la porte d'entrée.

L'Action : Vous poussez la porte pour l'ouvrir.
La Conséquence : La porte est maintenant ouverte.
La Nouvelle Promesse : Parce que vous avez ouvert la porte, vous avez maintenant une promesse (une obligation) de la refermer plus tard.

Dans les anciens modèles informatiques, le système savait que la porte était ouverte, mais il ne comprenait pas automatiquement que vous aviez maintenant une nouvelle règle à suivre. Les auteurs ont trouvé comment faire réaliser à l'ordinateur : « Ah, l'Agent X vient d'ouvrir la porte. Par conséquent, l'Agent X est désormais soumis à une nouvelle règle : "Doit fermer la porte". »

3. La Solution : La Carte des « Mondes Possibles »

Pour suivre ces promesses, les auteurs utilisent un concept appelé Mondes Possibles.

L'Analogie :
Imaginez que votre situation actuelle est de se tenir sur un chemin unique. Mais parce que vous avez une promesse à tenir, l'ordinateur imagine une multitude de chemins parallèles (mondes possibles) qui bifurquent de là où vous êtes.

Dans certains de ces chemins, vous pourriez oublier de fermer la porte.
Dans d'autres, vous pourriez la fermer immédiatement.
Dans d'autres encore, vous pourriez la fermer lentement.

La règle de l'ordinateur est : « Une promesse n'est valide que si elle est vraie dans TOUS les chemins possibles qui suivent. »

S'il existe ne serait-ce qu'un seul chemin où vous laissez la porte ouverte pour toujours, la promesse est rompue. Les auteurs ont créé une « carte » spéciale (appelée un fluent nommé O) qui relie votre situation actuelle à tous ces futurs chemins possibles.

4. Comment l'Ordinateur Suit les Changements

Le document résout le « problème du cadre » pour ces promesses en créant trois types de règles pour la façon dont la carte change lorsqu'on effectue une action :

Type A : Le Mouvement Banale (Actions Non-Produisant pas d'Obligation)
- Exemple : Vous marchez vers la cuisine.
- Effet : La carte des futurs possibles se déplace légèrement (vous êtes maintenant dans la cuisine dans tous ces chemins), mais aucune nouvelle promesse n'est créée, et aucune ancienne promesse ne disparaît. La promesse « Doit fermer la porte » reste exactement la même.
Type B : Le Tueur de Promesse (Actions Libérant une Obligation)
- Exemple : Vous fermez enfin la porte.
- Effet : L'ordinateur regarde la carte et dit : « Dans chaque futur chemin possible, la porte est fermée. » Puisque la promesse est remplie, l'ordinateur efface la règle « Doit fermer la porte » de la carte. L'obligation est partie.
Type C : Le Créateur de Promesse (Actions Produisant une Obligation)
- Exemple : Vous ouvrez la porte.
- Effet : L'ordinateur regarde la carte et dit : « Oh non ! Dans certains de ces chemins, la porte reste ouverte. » Il trace immédiatement une nouvelle ligne sur la carte : « À partir de ce point, dans chaque chemin valide, la porte doit être fermée. » Une nouvelle obligation est née.

5. L'Astuce de la « Régression » : Regarder vers l'Arrière

Le document introduit également une astuce ingénieuse appelée Régression.

L'Analogie :
Imaginez que vous regardez un film et que vous voulez savoir si un personnage tiendra une promesse à la toute fin. Au lieu de regarder tout le film vers l'avant, l'ordinateur travaille vers l'arrière.

Il commence par la scène finale.
Il demande : « Que devait-t-il se passer dans la scène précédente pour que la promesse soit respectée ? »
Il continue de rembobiner la cassette, étape par étape, jusqu'à atteindre la toute première scène (le début du film).

Cela permet à l'ordinateur de prouver si une promesse est valide en regardant uniquement les conditions initiales, plutôt qu'en simulant chaque seconde du futur.

Résumé

Ce document est un manuel technique pour apprendre aux ordinateurs à gérer des promesses de type juridique dans un monde dynamique.

Il corrige le problème de savoir ce qui reste identique lorsqu'une promesse est faite.
Il crée un système où faire une action spécifique (comme ouvrir une porte) crée automatiquement une nouvelle règle (fermer la porte).
Il fournit un moyen mathématique de vérifier si ces règles sont respectées en remontant le fil du temps jusqu'au début.

Les auteurs affirment que c'est une méthode plus simple et plus propre que les méthodes précédentes, éliminant la complexité inutile concernant les « mondes idéaux » pour s'en tenir à une carte claire et logique de ce qui est possible et de ce qui est requis.

Résumé technique : Actions génératrices d'obligations dans le calcul des situations

Énoncé du problème

L'article traite du problème du cadre (frame problem) dans le contexte des actions génératrices d'obligations au sein du calcul des situations. Alors que les travaux fondateurs de Raymond Reiter ont fourni une solution au problème du cadre pour les actions ordinaires (via les axiomes d'état successeur) et que Scherl et Levesque ont étendu cela aux actions génératrices de connaissances, un cadre complet pour les actions génératrices d'obligations est resté sous-développé.

Plus précisément, les auteurs identifient une lacune dans les travaux de Demolombe et al. [6], qui ont introduit des concepts déontiques dans le calcul des situations mais n'ont pas développé de cadre complet pour le raisonnement sur ces actions ou pour l'implémentation de spécifications. Le défi central consiste à modéliser formellement des actions qui créent des obligations pour l'agent qui les accomplit (par exemple, déverrouiller une porte crée l'obligation de la verrouiller plus tard) et à déterminer comment ces obligations persistent, changent ou se terminent à mesure que l'agent accomplit des actions ultérieures, sans avoir à énumérer explicitement tous les faits légaux non affectés.

Méthodologie

Les auteurs proposent une solution fondée sur les théories d'actions de base de Reiter et la sémantique des mondes possibles de type Kripke pour la logique déontique, évitant ainsi l'ordonnancement par « idéalité » des situations utilisé dans les formulations précédentes.

1. Cadre formel

L'approche utilise une version temporelle du calcul des situations avec des sortes pour les actions, les situations, les points temporels et les objets.

Fluent déontique ( $O$ ) : Une relation binaire $O(s', s)$ est introduite, indiquant que la situation $s'$ est déontiquement accessible à partir de la situation $s$ .
Opérateur d'obligation : Une obligation $Oblg(\phi, s)$ est définie comme un opérateur de nécessité sur la relation d'accessibilité : $(\forall s'). O(s', s) \supset \phi[s']$ . Cela signifie que $\phi$ est obligatoire dans $s$ si elle est vérifiée dans toutes les situations déontiquement accessibles.
Classification des actions : Les actions sont classées en trois types concernant leur effet sur les obligations :
1. Actions non génératrices d'obligations : Actions ordinaires qui ne créent ni ne libèrent d'obligations.
2. Actions de libération d'obligations : Actions qui interrompent les obligations existantes (par exemple, notifier un responsable après avoir verrouillé une porte).
3. Actions génératrices d'obligations : Actions qui créent de nouvelles obligations (par exemple, déverrouiller une porte crée l'obligation de la verrouiller).

2. Axiomes d'état successeur pour $O$

La contribution technique centrale est la dérivation d'un axiome d'état successeur (SSA) pour le fluent déontique $O$ . Cet axiome caractérise la manière dont l'ensemble des situations déontiquement accessibles change après qu'une action $a$ a été accomplie dans une situation $s$ :

Pour les actions non génératrices d'obligations : Les situations accessibles dans l'état successeur sont simplement les images des situations accessibles de l'état actuel sous l'action $a$ .
Pour les actions de libération d'obligations : L'axiome filtre les situations accessibles où la condition de l'obligation (le fluent associé) a été satisfaite, éliminant ainsi ces chemins de l'espace déontique.
Pour les actions génératrices d'obligations : L'axiome restreint les situations accessibles à celles où la nouvelle obligation créée est satisfaite. Plus précisément, si l'action $a$ crée une obligation pour le fluent $F$ , les nouvelles situations accessibles sont celles où $F$ est vrai.

3. Régression pour les obligations

L'article étend l'opérateur de régression de Reiter pour gérer les formules d'obligation. Cela permet de réduire le raisonnement sur la vérité des énoncés d'obligation dans des situations futures au raisonnement sur la situation initiale ( $S_0$ ).

Les auteurs définissent un opérateur de régression $R$ qui gère le prédicat $Oblg$.
L'opérateur transforme de manière récursive les formules impliquant des obligations dans les situations successeurs en formules équivalentes dans la situation initiale, en utilisant les axiomes d'état successeur pour les fluents ordinaires et pour le fluent déontique $O$ .
Un théorème de régression est prouvé, stipulant qu'une phrase $W$ est impliquée par une théorie d'action de base si et seulement si sa forme entièrement régressée est impliquée par la situation initiale augmentée des axiomes de nom unique et des propriétés spécifiques de la relation $O$ (telles que la sérialité et la réflexivité).

Contributions clés

Formalisation simplifiée : L'article simplifie la caractérisation de la relation d'accessibilité en éliminant la notion d'« idéalité » des situations, s'alignant ainsi plus étroitement sur la sémantique Kripke standard de la logique déontique (notamment la Logique Déontique Standard).
Théorie d'action complète : Il fournit un ensemble complet d'axiomes (fondamentaux, de précondition, d'état successeur et de noms uniques) étendant le cadre de Reiter pour inclure les actions génératrices d'obligations.
Preuves de correction : Les auteurs prouvent que leur formalisation produit des propriétés intuitives :
- Création : Accomplir une action génératrice d'obligations crée l'obligation correspondante dans la situation successeur.
- Persistance : Les obligations persistent dans les situations suivantes à moins qu'elles ne soient explicitement arrêtées.
- Terminaison : Les obligations sont supprimées lorsque le fluent associé devient vrai (ou lorsqu'une action de libération spécifique est effectuée).
Extension de la régression : L'article étend le théorème de régression au domaine des obligations, permettant le raisonnement automatisé sur les contrats juridiques et les contrats intelligents (smart contracts) au sein du calcul des situations.

Résultats

L'article démontre que la formalisation proposée modélise correctement la dynamique des obligations. En utilisant un exemple courant de scénario d'ouverture de porte (déverrouiller, verrouiller et notifier un responsable), les auteurs montrent :

Comment la relation d'accessibilité $O$ évolue à mesure que les actions sont accomplies.
Comment l'opérateur de régression parvient avec succès à réduire des requêtes d'obligations complexes dans des situations futures en conditions vérifiables dans la situation initiale.
Le système permet de vérifier des propriétés telles que « si une phrase est obligatoire dans une situation, elle le reste dans les situations suivantes, à moins que l'obligation ne soit explicitement arrêtée ».

Signification et revendications

Les auteurs affirment que ce travail fournit une base sémantique rigide pour la spécification et le raisonnement automatisé des documents juridiques et des contrats juridiques intelligents. En formalisant les obligations directement dans le calcul des situations, l'approche :

Évite le besoin d'étapes de compilation supplémentaires requises par d'autres approches (par exemple, les méthodes basées sur les contraintes).
Tire parti d'outils existants comme GOLOG (un langage de programmation basé sur le calcul des situations) pour définir des actions complexes et vérifier des accords juridiques.
Offre une solution au problème du cadre spécifiquement adaptée à la logique déontique, garantissant que les agents de raisonnement juridique peuvent suivre les changements de droits et de devoirs sans altérer accidentellement des faits juridiques non liés.

L'article se positionne comme une étape nécessaire vers la mise en œuvre de contrats juridiques intelligents pouvant être formellement vérifiés pour leur cohérence et leur exécution fiable dans des environnements dynamiques et distribués. Les travaux futurs sont identifiés comme l'extension de ce cadre pour gérer les violations de normes et les obligations contraires au devoir (contrary-to-duty obligations).