The situation calculus is a logic formalism designed for representing and reasoning about dynamical domains.
[1] The main version of the situational calculus that is presented in this article is based on that introduced by Ray Reiter in 1991.
The situation calculus represents changing scenarios as a set of first-order logic formulae.
The basic elements of the calculus are: A domain is formalized by a number of formulae, namely: A simple robot world will be modeled as a running example.
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.
While actions, situations, and objects are elements of the domain, the fluents are modeled as either predicates or functions.
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: The situation before any actions have been performed is typically denoted
Statements whose truth value may change are modeled by relational fluents, predicates that take a situation as their final argument.
In the example, the condition that dropping an object is only possible when one is carrying it is modeled by: 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 heavy): Given that an action is possible in a situation, one must specify the effects of that action on the fluents.
The following models that some objects are fragile (indicated by the predicate fragile) and dropping them causes them to be broken (indicated by the fluent broken): 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.
For example, it is not possible to deduce that after picking up an object, the robot's location remains unchanged.
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.
can be written in generalised form as a positive and a negative effect axiom: The formula
If this pair of axioms describe all the ways in which fluent F can change value, they can be rewritten as a single axiom: In words, this formula states: "given that it is possible to perform action a in situation s, the fluent F would be true in the resulting situation
The following statements model that initially, the robot carries nothing, is at location
By iterating this procedure, one can end up with an equivalent formula containing only the initial situation S0.
GOLOG is a logic programming language based on the situation calculus.
Originally, situations were defined as "the complete state of the universe at an instant of time".
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 order for inertia to hold, formulae called frame axioms are needed.
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 s to mean the initial situation and making statements about it (e.g.,
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 x in the situation s) and for an attempt to use circumscription to replace the frame axioms.
It is also possible (e.g. Kowalski 1979, Apt and Bezem 1990, Shanahan 1997) to write the situation calculus as a logic program: Here Holds is a meta-predicate and the variable f ranges over fluents.
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.