Calcul de situation - Situation calculus

Le calcul de situation est un formalisme logique conçu pour représenter et raisonner sur des domaines dynamiques. Il a été introduit pour la première fois par John McCarthy en 1963. La version principale du calcul situationnel qui est présentée dans cet article est basée sur celle introduite par Ray Reiter en 1991. Elle est suivie par des sections sur la version 1986 de McCarthy et une formulation de programmation logique .

Aperçu

Le calcul de situation représente des scénarios changeants sous la forme d'un ensemble de formules logiques de premier ordre . Les éléments de base du calcul sont:

  • Les actions qui peuvent être effectuées dans le monde
  • Les fluides qui décrivent l'état du monde
  • Les situations

Un domaine est formalisé par un certain nombre de formules, à savoir:

  • Axiomes préalables à l'action, un pour chaque action
  • Axiomes d'état successeur, un pour chaque courant
  • Axiomes décrivant le monde dans diverses situations
  • Les axiomes fondateurs du calcul de situation

Un monde de robot simple sera modélisé comme un exemple courant. Dans ce monde, il y a un seul robot et plusieurs objets inanimés. Le monde est disposé selon une grille afin que les emplacements puissent être spécifiés en termes de points de coordonnées. Il est possible pour le robot de se déplacer à travers le monde et de ramasser et de déposer des objets. Certains objets peuvent être trop lourds à ramasser par le robot ou fragiles au point de se casser en cas de chute. Le robot a également la capacité de réparer tous les objets cassés qu'il tient.

Éléments

Les principaux éléments du calcul de situation sont les actions, les fluides et les situations. Un certain nombre d'objets sont également généralement impliqués dans la description du monde. Le calcul de situation est basé sur un domaine trié avec trois sortes: actions, situations et objets, où les objets incluent tout ce qui n'est pas une action ou une situation. Des variables de chaque sorte peuvent être utilisées. Alors que les actions, les situations et les objets sont des éléments du domaine, les fluents sont modélisés sous forme de prédicats ou de fonctions.

Actions

Les actions forment une sorte de domaine. Des variables d'action de tri peuvent être utilisées. Les actions peuvent être quantifiées. Dans l'exemple du monde du robot, les termes d'action possibles seraient de modéliser le robot se déplaçant vers un nouvel emplacement et de modéliser le robot ramassant un objet . Un prédicat spécial est utilisé pour indiquer lorsqu'une action est exécutable.

Situations

Dans le calcul de situation, un monde dynamique est modélisé comme progressant à travers une série de situations à la suite de diverses actions exécutées dans le monde. Une situation représente un historique des événements d'action. Dans la version Reiter du calcul de situation décrit ici, une situation ne représente pas un état, contrairement au sens littéral du terme et contrairement à la définition originale de McCarthy et Hayes. Ce point a été résumé par Reiter comme suit:

Une situation est une séquence finie d'actions. Période. Ce n'est pas un état, ce n'est pas un instantané, c'est une histoire [1] .

La situation avant l'exécution de toute action est généralement désignée et appelée situation initiale. La nouvelle situation résultant de l'exécution d'une action est indiquée à l'aide du symbole de fonction (certaines autres références l'utilisent également ). Ce symbole de fonction a une situation et une action comme arguments, et une situation en conséquence, cette dernière étant la situation qui résulte de l'exécution de l'action donnée dans la situation donnée.

Le fait que les situations soient des séquences d'actions et non des états est imposé par un axiome qui est égal à si et seulement si et . Cette condition n'a aucun sens si les situations étaient des états, car deux actions différentes exécutées dans deux états différents peuvent aboutir au même état.

Dans l'exemple du monde du robot, si la première action du robot est de se déplacer vers l'emplacement , la première action est et la situation qui en résulte est . Si sa prochaine action est de ramasser la balle, la situation qui en résulte est . Les termes de situations comme et désignent les séquences d'actions exécutées, et non la description de l'état résultant de l'exécution.

Fluents

Les énoncés dont la valeur de vérité peut changer sont modélisés par des fluents relationnels , des prédicats qui prennent une situation comme argument final. Les fluides fonctionnels sont également possibles , des fonctions qui prennent une situation comme argument final et renvoient une valeur dépendante de la situation. Les fluides peuvent être considérés comme des «propriétés du monde» ».

Dans l'exemple, le courant peut être utilisé pour indiquer que le robot porte un objet particulier dans une situation particulière. Si le robot ne transporte initialement rien, est faux alors que est vrai. L'emplacement du robot peut être modélisé à l'aide d'un fluide fonctionnel qui renvoie l'emplacement du robot dans une situation particulière.

Formules

La description d'un monde dynamique est codée dans des logiques de second ordre à l' aide de trois types de formules: des formules sur les actions (conditions préalables et effets), des formules sur l'état du monde et des axiomes fondateurs.

Conditions préalables à l'action

Certaines actions peuvent ne pas être exécutables dans une situation donnée. Par exemple, il est impossible de déposer un objet à moins que l'on ne le porte. Les restrictions sur la performance des actions sont modélisées par des littéraux de la forme , où est une action, une situation, et est un prédicat binaire spécial indiquant l'exécutabilité des actions. Dans l'exemple, la condition selon laquelle déposer un objet n'est possible que lorsque l'on le transporte est modélisée par:

A titre d'exemple plus complexe, les modèles suivants que le robot ne peut transporter qu'un seul objet à la fois, et que certains objets sont trop lourds pour que le robot puisse les soulever (indiqués par le prédicat ):

Effets d'action

Étant donné qu'une action est possible dans une situation, il faut préciser les effets de cette action sur les fluents. Ceci est fait par les axiomes d'effet. Par exemple, le fait que ramasser un objet amène le robot à le transporter peut être modélisé comme:

Il est également possible de spécifier des effets conditionnels, qui sont des effets qui dépendent de l'état actuel. Les modèles suivants indiquent que certains objets sont fragiles (indiqués par le prédicat ) et les laisser tomber provoque leur rupture (indiqué par le courant ):

Bien que cette formule décrit correctement l'effet des actions, elle n'est pas suffisante pour décrire correctement l'action en logique, en raison du problème de cadre .

Le problème du cadre

Bien que les formules ci-dessus semblent appropriées pour raisonner sur les effets des actions, elles présentent une faiblesse critique - elles ne peuvent pas être utilisées pour dériver les non-effets des actions. Par exemple, il n'est pas possible de déduire qu'après avoir ramassé un objet, l'emplacement du robot reste inchangé. Cela nécessite un soi-disant axiome cadre, une formule comme:

Le besoin de spécifier des axiomes de trame a longtemps été reconnu comme un problème dans l'axiomatisation des mondes dynamiques, et est connu comme le problème de trame . Comme il existe généralement un très grand nombre de tels axiomes, il est très facile pour le concepteur de laisser de côté un axiome de cadre nécessaire, ou d'oublier de modifier tous les axiomes appropriés lors d'un changement dans la description du monde.

Les axiomes de l'état successeur

Les axiomes d'état successeur "résolvent" le problème de cadre dans le calcul de situation. Selon cette solution, le concepteur doit énumérer comme axiomes d'effet toutes les façons dont la valeur d'un courant particulier peut être modifiée. Les axiomes d'effet affectant la valeur de fluent peuvent être écrits sous forme généralisée sous la forme d'un axiome d'effet positif et négatif:

La formule décrit les conditions dans lesquelles l'action en situation fait que le courant devient vrai dans la situation successeur . De même, décrit les conditions dans lesquelles l'exécution d'une action en situation rend couramment faux dans la situation successeur.

Si cette paire d'axiomes décrivent toutes les façons dont le fluent peut changer de valeur, ils peuvent être réécrits en un seul axiome:

En d'autres termes, ce document fait état de la formule: « étant donné qu'il est possible d'effectuer une action dans la situation , le Fluent serait vrai dans la situation qui en résulte si et seulement si l' exécution en RENDRAIT vrai, ou il est vrai dans la situation et l' exécution en serait pas le rendre faux. "

A titre d'exemple, la valeur du fluent introduit ci-dessus est donnée par l'axiome d'état successeur suivant:

États

Les propriétés de la situation initiale ou de toute autre situation peuvent être spécifiées en les énonçant simplement sous forme de formules. Par exemple, un fait sur l'état initial est formalisé en faisant des affirmations sur (qui n'est pas un état, mais une situation ). Les déclarations suivantes indiquent qu'au départ, le robot ne porte rien, est à l'emplacement et il n'y a pas d'objets cassés:

Axiomes fondamentaux

Les axiomes fondateurs du calcul de situation formalisent l'idée que les situations sont des histoires par avoir . Ils incluent également d'autres propriétés comme l'induction du second ordre sur des situations.

Régression

La régression est un mécanisme permettant de prouver les conséquences dans le calcul de situation. Il est basé sur l'expression d'une formule contenant la situation en termes d'une formule contenant l'action et la situation , mais pas la situation . En répétant cette procédure, on peut se retrouver avec une formule équivalente ne contenant que la situation initiale . Prouver les conséquences est censé être plus simple à partir de cette formule que de la formule originale.

GOLOG

GOLOG est un langage de programmation logique basé sur le calcul de situation.

La version originale du calcul de situation

La principale différence entre le calcul de situation d'origine de McCarthy et Hayes et celui utilisé aujourd'hui est l'interprétation des situations. Dans la version moderne du calcul situationnel, une situation est une séquence d'actions. À l'origine, les situations étaient définies comme «l'état complet de l'univers à un instant du temps». Il était clair dès le départ que de telles situations ne pouvaient pas être complètement décrites; l'idée était simplement de faire quelques déclarations sur des situations et d'en tirer des conséquences. Ceci est également différent de l'approche adoptée par le calcul fluide , où un état peut être un ensemble de faits connus, c'est-à-dire une description éventuellement incomplète de l'univers.

Dans la version originale du calcul de situation, les fluides ne sont pas réifiés. En d'autres termes, les conditions qui peuvent changer sont représentées par des prédicats et non par des fonctions. En fait, McCarthy et Hayes ont défini un fluent comme une fonction qui dépend de la situation, mais ils ont ensuite continué en utilisant toujours des prédicats pour représenter les fluents. Par exemple, le fait qu'il pleut sur place dans la situation est représenté par le littéral . Dans la version de 1986 du calcul de situation de McCarthy, les fluides fonctionnels sont utilisés. Par exemple, la position d'un objet dans la situation est représentée par la valeur de , où est une fonction. Des déclarations sur de telles fonctions peuvent être données en utilisant l'égalité: signifie que l'emplacement de l'objet est le même dans les deux situations et .

L'exécution des actions est représentée par la fonction : l'exécution de l'action dans la situation est la situation . Les effets des actions sont exprimés par des formules mettant en relation fluides en situation et fluents en situations . Par exemple, le fait que l'action d'ouverture de la porte entraîne l'ouverture de la porte si elle n'est pas verrouillée est représenté par:

Les prédicats et représentent les conditions de verrouillage et d'ouverture d'une porte, respectivement. Puisque ces conditions peuvent varier, elles sont représentées par des prédicats avec un argument de situation. La formule dit que si la porte n'est pas verrouillée dans une situation, alors la porte est ouverte après l'exécution de l'action d'ouverture, cette action étant représentée par la constante .

Ces formules ne sont pas suffisantes pour dériver tout ce qui est considéré comme plausible. En effet, les fluides à différentes situations ne sont liés que s'ils sont des conditions préalables et des effets d'actions; si un fluent n'est pas affecté par une action, il n'y a aucun moyen de déduire qu'il n'a pas changé. Par exemple, la formule ci-dessus n'implique pas que cela découle de , ce à quoi on pourrait s'attendre (la porte n'est pas verrouillée en l'ouvrant). Pour que l'inertie soit maintenue, des formules appelées axiomes de trame sont nécessaires. Ces formules spécifient tous les non-effets des actions:

Dans la formulation originale du calcul de situation, la situation initiale, désignée plus tard par , n'est pas explicitement identifiée. La situation initiale n'est pas nécessaire si les situations sont considérées comme des descriptions du monde. Par exemple, pour représenter le scénario dans lequel la porte était fermée mais non verrouillée et l'action d'ouverture, elle est effectuée est formalisée en prenant une constante pour signifier la situation initiale et en faisant des déclarations à ce sujet (par exemple, ). Le fait que la porte soit ouverte après le changement est reflété par la formule impliquée. La situation initiale est plutôt nécessaire si, comme dans le calcul de situation moderne, une situation est considérée comme une histoire d'actions, car la situation initiale représente la séquence vide d'actions.

La version du calcul de situation introduite par McCarthy en 1986 diffère de la version originale pour l'utilisation de fluents fonctionnels (par exemple, est un terme représentant la position de dans la situation ) et pour une tentative d'utiliser la circonscription pour remplacer les axiomes du cadre.

Le calcul de situation comme programme logique

Il est également possible (par exemple Kowalski 1979, Apt et Bezem 1990, Shanahan 1997) d'écrire le calcul de situation comme un programme logique:

Voici un méta-prédicat et la variable varie sur les fluents. Les prédicats , et correspondent aux prédicats , et respectivement. La flèche gauche représente la moitié de l'équivalence . L'autre moitié est implicite dans l'achèvement du programme, dans lequel la négation est interprétée comme une négation comme un échec . Les axiomes d'induction sont également implicites et ne sont nécessaires que pour prouver les propriétés du programme. Le raisonnement en arrière comme dans la résolution SLD , qui est le mécanisme habituel utilisé pour exécuter des programmes logiques, implémente la régression de manière implicite.

Voir également

Les références

  • J. McCarthy et P. Hayes (1969). Quelques problèmes philosophiques du point de vue de l'intelligence artificielle . Dans B. Meltzer et D. Michie, éditeurs, Machine Intelligence , 4: 463–502. Édimbourg University Press, 1969.
  • R. Kowalski (1979). Logique de résolution de problèmes - Elsevier North Holland.
  • KR Apt et M. Bezem (1990). Programmes acycliques. Dans: 7e Conférence internationale sur la programmation logique. MIT Press. Jérusalem, Israël.
  • R. Reiter (1991). Le problème du cadre dans le calcul de situation: une solution simple (parfois) et un résultat d'exhaustivité pour la régression des objectifs. Dans Vladimir Lifshitz, rédacteur en chef, Intelligence artificielle et théorie mathématique du calcul: articles en l'honneur de John McCarthy , pages 359-380, San Diego, Californie, États-Unis. Professionnel de la presse académique, Inc. 1991.
  • M. Shanahan (1997). Résolution du problème du cadre: une étude mathématique de la loi du sens commun de l'inertie. MIT Press.
  • H. Levesque, F. Pirri et R. Reiter (1998). Fondements pour le calcul de la situation . Transactions électroniques sur l'intelligence artificielle , 2 (3-4): 159-178.
  • F. Pirri et R. Reiter (1999). Quelques contributions à la métathéorie du Situation Calculus. Journal de l'ACM , 46 (3): 325–361. doi : 10.1145 / 316542.316545
  • R. Reiter (2001). Connaissance en action: fondements logiques pour la spécification et la mise en œuvre de systèmes dynamiques. La presse du MIT.