Personal tools

Situation calculus

From Wikipedia, the free encyclopedia

Jump to: navigation, search

The situation calculus is a logic formalism designed for representing and reasoning about dynamical domains. It was first introduced by John McCarthy in 1963.[1] The main version of the situational calculus that is presented in this article is based on that introduced by Ray Reiter in 1991. It is followed by sections about McCarthy's 1986 version and a logic programming formulation.

Overview

The situation calculus represents changing scenarios as a set of first-order logic formulae. The basic elements of the calculus are:

  • The actions that can be performed in the world
  • The fluents that describe the state of the world
  • The situations

A domain is formalized by a number of formulae, namely:

  • Action precondition axioms, one for each action
  • Successor state axioms, one for each fluent
  • Axioms describing the world in various situations
  • The foundational axioms of the situation calculus

A simple robot world will be modeled as a running example. In this world there is a single robot and several inanimate objects. The world is laid out according to a grid so that locations can be specified in terms of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x,y)} coordinate points. It is possible for the robot to move around the world, and to pick up and drop items. Some items may be too heavy for the robot to pick up, or fragile so that they break when they are dropped. The robot also has the ability to repair any broken items that it is holding.

Elements

The main elements of the situation calculus are the actions, fluents and the situations. A number of objects are also typically involved in the description of the world. The situation calculus is based on a sorted domain with three sorts: actions, situations, and objects, where the objects include everything that is not an action or a situation. Variables of each sort can be used. While actions, situations, and objects are elements of the domain, the fluents are modeled as either predicates or functions.

Actions

The actions form a sort of the domain. Variables of sort action can be used and also functions whose result is of sort action. Actions can be quantified. In the example robot world, possible action terms would be Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle move(x,y)} to model the robot moving to a new location Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x,y)} , and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle pickup(o)} to model the robot picking up an object Template:Mvar. A special predicate Template:Mvar is used to indicate when an action is executable.

Situations

In the situation calculus, a dynamic world is modeled as progressing through a series of situations as a result of various actions being performed within the world. A situation represents a history of action occurrences. In the Reiter version of the situation calculus described here, a situation does not represent a state, contrarily to the literal meaning of the term and contrarily to the original definition by McCarthy and Hayes. This point has been summarized by Reiter as follows:

A situation is a finite sequence of actions. Period. It's not a state, it's not a snapshot, it's a history.[2]

The situation before any actions have been performed is typically denoted Template:Tmath and called the initial situation. The new situation resulting from the performance of an action is denoted using the function symbol Template:Mvar (Some other references[3] also use Template:Mvar). This function symbol has a situation and an action as arguments, and a situation as a result, the latter being the situation that results from performing the given action in the given situation.

The fact that situations are sequences of actions and not states is enforced by an axiom stating that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)} is equal to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a',s')} if and only if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a=a'} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle s=s'} . This condition makes no sense if situations were states, as two different actions executed in two different states can result in the same state.

In the example robot world, if the robot's first action is to move to location Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (2,3)} , the first action is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle move(2,3)} and the resulting situation is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(move(2,3),S_{0})} . If its next action is to pick up the ball, the resulting situation is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))} . Situations terms like Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(move(2,3),S_{0})} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))} denote the sequences of executed actions, and not the description of the state that result from execution.

Fluents

Statements whose truth value may change are modeled by relational fluents, predicates that take a situation as their final argument. Also possible are functional fluents, functions that take a situation as their final argument and return a situation-dependent value. Fluents may be thought of as "properties of the world"'.

In the example, the fluent Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{isCarrying}(o,s)} can be used to indicate that the robot is carrying a particular object in a particular situation. If the robot initially carries nothing, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{isCarrying}(Ball,S_{0})} is false while Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{isCarrying}(Ball,do(pickup(Ball),S_{0}))} is true. The location of the robot can be modeled using a functional fluent Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle location(s)} that returns the location Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x,y)} of the robot in a particular situation.

Formulae

The description of a dynamic world is encoded in second-order logic using three kinds of formulae: formulae about actions (preconditions and effects), formulae about the state of the world, and foundational axioms.

Action preconditions

Some actions may not be executable in a given situation. For example, it is impossible to put down an object unless one is in fact carrying it. The restrictions on the performance of actions are modeled by literals of the form Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{Poss}(a,s)} , where Template:Mvar is an action, Template:Mvar a situation, and Template:Mvar is a special binary predicate denoting executability of actions. In the example, the condition that dropping an object is only possible when one is carrying it is modeled by:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{Poss}(drop(o),s)\leftrightarrow \textit{isCarrying}(o,s) }

As a more complex example, the following models that the robot can carry only one object at a time, and that some objects are too heavy for the robot to lift (indicated by the predicate Template:Mvar):

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{Poss}(pickup(o),s)\leftrightarrow(\forall z\ \neg \textit{isCarrying}(z,s))\wedge\neg heavy(o) }

Action effects

Given that an action is possible in a situation, one must specify the effects of that action on the fluents. This is done by the effect axioms. For example, the fact that picking up an object causes the robot to be carrying it can be modeled as:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(pickup(o),s)\rightarrow \textit{isCarrying}(o,do(pickup(o),s)) }

It is also possible to specify conditional effects, which are effects that depend on the current state. The following models that some objects are fragile (indicated by the predicate Template:Mvar) and dropping them causes them to be broken (indicated by the fluent Template:Mvar):

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(drop(o),s)\wedge fragile(o)\rightarrow broken(o,do(drop(o),s)) }

While this formula correctly describes the effect of the actions, it is not sufficient to correctly describe the action in logic, because of the frame problem.

The frame problem

While the above formulae seem suitable for reasoning about the effects of actions, they have a critical weakness—they cannot be used to derive the non-effects of actions. For example, it is not possible to deduce that after picking up an object, the robot's location remains unchanged. This requires a so-called frame axiom, a formula like:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(pickup(o),s)\wedge location(s)=(x,y)\rightarrow location(do(pickup(o),s))=(x,y) }

The need to specify frame axioms has long been recognised as a problem in axiomatizing dynamic worlds, and is known as the frame problem. As there are generally a very large number of such axioms, it is very easy for the designer to leave out a necessary frame axiom, or to forget to modify all appropriate axioms when a change to the world description is made.

The successor state axioms

The successor state axioms "solve" the frame problem in the situation calculus. According to this solution, the designer must enumerate as effect axioms all the ways in which the value of a particular fluent can be changed. The effect axioms affecting the value of fluent Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F(\overrightarrow{x},s)} can be written in generalised form as a positive and a negative effect axiom:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(a,s)\wedge\gamma_{F}^{+}(\overrightarrow{x},a,s)\rightarrow F(\overrightarrow{x},do(a,s)) }
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(a,s)\wedge\gamma_{F}^{-}(\overrightarrow{x},a,s)\rightarrow\neg F(\overrightarrow{x},do(a,s)) }

The formula Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \gamma_{F}^{+}} describes the conditions under which action Template:Mvar in situation Template:Mvar makes the fluent Template:Mvar become true in the successor situation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)} . Likewise, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \gamma_{F}^{-}} describes the conditions under which performing action Template:Mvar in situation Template:Mvar makes fluent Template:Mvar false in the successor situation.

If this pair of axioms describe all the ways in which fluent Template:Mvar can change value, they can be rewritten as a single axiom:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(a,s)\rightarrow\left[F(\overrightarrow{x},do(a,s))\leftrightarrow\gamma_{F}^{+}(\overrightarrow{x},a,s)\vee\left(F(\overrightarrow{x},s)\wedge\neg\gamma_{F}^{-}(\overrightarrow{x},a,s)\right)\right] }

In words, this formula states: "given that it is possible to perform action Template:Mvar in situation Template:Mvar, the fluent Template:Mvar would be true in the resulting situation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)} if and only if performing Template:Mvar in Template:Mvar would make it true, or it is true in situation Template:Mvar and performing Template:Mvar in Template:Mvar would not make it false."

By way of example, the value of the fluent Template:Mvar introduced above is given by the following successor state axiom:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Poss(a,s) \rightarrow \left[ broken(o,do(a,s)) \leftrightarrow a=drop(o)\wedge fragile(o) \vee broken(o,s) \wedge a \neq repair(o) \right] }

States

The properties of the initial or any other situation can be specified by simply stating them as formulae. For example, a fact about the initial state is formalized by making assertions about Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S_{0}} (which is not a state, but a situation). The following statements model that initially, the robot carries nothing, is at location Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (0,0)} , and there are no broken objects:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall z\,\neg \textit{isCarrying}(z,S_{0}) }
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle location(S_{0})=(0,0)\, }
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall o\,\neg broken(o,S_{0}) }

Foundational axioms

The foundational axioms of the situation calculus formalize the idea that situations are histories by having Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)=do(a',s') \iff a=a' \land s=s'} . They also include other properties such as the second-order induction on situations.

Regression

Regression[4] is a mechanism for proving consequences in the situation calculus.[5] It is based on expressing a formula containing the situation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)} in terms of a formula containing the action Template:Mvar and the situation Template:Mvar, but not the situation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle do(a,s)} . By iterating this procedure, one can end up with an equivalent formula containing only the initial situation Template:Mvar. Proving consequences is supposedly simpler from this formula than from the original one.

GOLOG

GOLOG is a logic programming language based on the situation calculus.[6][7]

The original version of the situation calculus

The main difference between the original situation calculus by McCarthy and Hayes and the one in use today is the interpretation of situations. In the modern version of the situational calculus, a situation is a sequence of actions. Originally, situations were defined as "the complete state of the universe at an instant of time". It was clear from the beginning that such situations could not be completely described; the idea was simply to give some statements about situations, and derive consequences from them. This is also different from the approach that is taken by the fluent calculus, where a state can be a collection of known facts, that is, a possibly incomplete description of the universe.

In the original version of the situation calculus, fluents are not reified. In other words, conditions that can change are represented by predicates and not by functions. Actually, McCarthy and Hayes defined a fluent as a function that depends on the situation, but they then proceeded always using predicates to represent fluents. For example, the fact that it is raining at place Template:Mvar in the situation Template:Mvar is represented by the literal Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle raining(x,s)} . In the 1986 version of the situation calculus by McCarthy, functional fluents are used. For example, the position of an object Template:Mvar in the situation Template:Mvar is represented by the value of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle location(x,s)} , where Template:Mvar is a function. Statements about such functions can be given using equality: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle location(x,s)=location(x,s')} means that the location of the object Template:Mvar is the same in the two situations Template:Mvar and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle s'} .

The execution of actions is represented by the function Template:Mvar: the execution of the action Template:Mvar in the situation Template:Mvar is the situation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{result}(a,s)} . The effects of actions are expressed by formulae relating fluents in situation Template:Mvar and fluents in situations Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \textit{result}(a,s)} . For example, that the action of opening the door results in the door being open if not locked is represented by:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \neg locked(door,s) \rightarrow open(door, \textit{result}(opens,s))}

The predicates Template:Mvar and Template:Mvar represent the conditions of a door being locked and open, respectively. Since these conditions may vary, they are represented by predicates with a situation argument. The formula says that if the door is not locked in a situation, then the door is open after executing the action of opening, this action being represented by the constant Template:Mvar.

These formulae are not sufficient to derive everything that is considered plausible. Indeed, fluents at different situations are only related if they are preconditions and effects of actions; if a fluent is not affected by an action, there is no way to deduce it did not change. For example, the formula above does not imply that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \neg locked(door,\textit{result}(opens,s))} follows from , which is what one would expect (the door is not made locked by opening it). In order for inertia to hold, formulae called frame axioms are needed. These formulae specify all non-effects of actions:

In the original formulation of the situation calculus, the initial situation, later denoted by Template:Tmath, is not explicitly identified. The initial situation is not needed if situations are taken to be descriptions of the world. For example, to represent the scenario in which the door was closed but not locked and the action of opening it is performed is formalized by taking a constant Template:Mvar to mean the initial situation and making statements about it (e.g., ). That the door is open after the change is reflected by formula being entailed. The initial situation is instead necessary if, like in the modern situation calculus, a situation is taken to be a history of actions, as the initial situation represents the empty sequence of actions.

The version of the situation calculus introduced by McCarthy in 1986 differs to the original one by the use of functional fluents (e.g., is a term representing the position of Template:Mvar in the situation Template:Mvar) and for an attempt to use circumscription to replace the frame axioms.

The situation calculus as a logic program

It is also possible (e.g. Kowalski 1979, Apt and Bezem 1990, Shanahan 1997) to write the situation calculus as a logic program:

Here Template:Mvar is a meta-predicate and the variable Template:Mvar ranges over fluents. The predicates Template:Mvar, Template:Mvar and Template:Mvar correspond to the predicates Template:Mvar, , and respectively. The left arrow ← is half of the equivalence ↔. The other half is implicit in the completion of the program, in which negation is interpreted as negation as failure. Induction axioms are also implicit, and are needed only to prove program properties. Backward reasoning as in SLD resolution, which is the usual mechanism used to execute logic programs, implements regression implicitly.

See also

References

  1. McCarthy, John (1963). "Situations, actions and causal laws" (PDF). Stanford University Technical Report. Archived from the original (PDF) on March 21, 2020.
  2. "ECSTER Debate Contribution".
  3. "Combining narratives, John McCarthy et al. (1998)" (PDF).
  4. Waldinger, Richard. "Achieving several goals simultaneously." In Readings in artificial intelligence, pp. 250-271. Morgan Kaufmann, 1981.
  5. Reiter, R., 1991. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. Artificial and Mathematical Theory of Computation, 3.
  6. Lakemeyer, Gerhard. "The Situation Calculus and Golog: A Tutorial" (PDF). www.hybrid-reasoning.org. Retrieved 16 July 2014.
  7. "Publications about GOLOG". Retrieved 16 July 2014.
  • J. McCarthy and P. Hayes (1969). Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence, 4:463–502. Edinburgh University Press, 1969.
  • R. Kowalski (1979). Logic for Problem Solving - Elsevier North Holland.
  • K.R. Apt and M. Bezem (1990). Acyclic Programs. In: 7th International Conference on Logic Programming. MIT Press. Jerusalem, Israel.
  • R. Reiter (1991). The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In Vladimir Lifshitz, editor, Artificial intelligence and mathematical theory of computation: papers in honour of John McCarthy, pages 359–380, San Diego, CA, USA. Academic Press Professional, Inc. 1991.
  • M. Shanahan (1997). Solving the Frame Problem: a Mathematical Investigation of the Common Sense Law of Inertia. MIT Press.
  • H. Levesque, F. Pirri, and R. Reiter (1998). Foundations for the situation calculus. Electronic Transactions on Artificial Intelligence, 2(3–4):159-178.
  • F. Pirri and R. Reiter (1999). Some contributions to the metatheory of the Situation Calculus. Journal of the ACM, 46(3):325–361. Template:Catalog lookup link
  • R. Reiter (2001). Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press.

Template:John McCarthy