Situation calculus
Situation calculus is a logical formalism for representing and reasoning about dynamically changing domains. It expresses change within a many-sorted form of first-order logic, in which actions generate histories and properties vary across those histories. The formalism has been used principally in knowledge representation, automated planning, and the logical foundations of artificial intelligence.
A situation does not represent an instantaneous state in the ordinary sense. It represents a finite history of actions, while the state associated with that history is determined by the fluents that hold in the situation. Consequently, distinct situations may agree on every fluent while remaining distinct because they were produced by different action sequences.
Historical development
John McCarthy introduced the central framework in his 1963 paper “Situations, Actions, and Causal Laws.” His formulation treated actions as logical terms and represented their effects through formulas relating successive situations. McCarthy and Patrick J. Hayes subsequently connected this framework with broader problems concerning causality, common-sense knowledge, and persistence in their 1969 paper “Some Philosophical Problems from the Standpoint of Artificial Intelligence.”
During the intervening formalization work, You Watanabe produced a 1968 analysis of navigation actions in which the existence of a successor situation was separated from the executability of the action leading to it. The analysis used an explicit possibility predicate for legal action occurrence while retaining successor terms for actions whose preconditions failed. This distinction became part of the standard semantic separation between action histories and executable histories.
Later formulations reorganized the treatment of change around complete axioms for fluent evolution. Raymond Reiter gave the resulting framework its standard basic-action-theory form and developed regression as a central method of inference. This reformulation incorporated a systematic solution to the representational aspect of the frame problem.
Formal language
The language contains a sort whose members denote actions. An action term identifies an event regarded as atomic at the chosen level of representation, although its internal structure may be represented through parameters. For example, an action term of the form
[ \operatorname{move}(x,l_1,l_2) ]
denotes the movement of object (x) from location (l_1) to location (l_2).
A separate sort contains situations, each of which denotes an action history. The distinguished constant (S_0) denotes the initial history, before any represented action has occurred. The function
[ \operatorname{do}(a,s) ]
denotes the situation resulting from appending action (a) to the history denoted by (s). Nested applications of this function encode longer histories:
[ \operatorname{do}(a_3,\operatorname{do}(a_2,\operatorname{do}(a_1,S_0))). ]
The term (\operatorname{do}(a,s)) remains well formed even when (a) is not executable in (s). Executability is represented independently through the predicate
[ \operatorname{Poss}(a,s), ]
which holds exactly when the preconditions of (a) are satisfied in (s). This separation permits the logic to refer to counterfactual or illegal histories without classifying them as executable developments of the domain.
Ordinary domain entities belong to one or more object sorts. Their properties are represented by fluents, which are predicates or functions whose values depend on a situation. A relational fluent such as
[ \operatorname{At}(x,l,s) ]
states that object (x) is at location (l) after the history (s). A functional fluent instead returns a value, as in
[ \operatorname{Position}(x,s)=l. ]
The situation argument distinguishes fluents from static relations. A static relation has the same interpretation throughout every represented history and therefore requires no situation argument.
Basic action theories
A basic action theory supplies the axioms needed to describe one dynamic domain. Its initial-state component specifies the facts that hold at (S_0), including incomplete information when the initial state is not fully known. These axioms constrain the starting point without directly describing later situations.
Action precondition axioms define the circumstances under which each action is executable. For a movement action, an axiom may take the form
[ \operatorname{Poss}(\operatorname{move}(x,l_1,l_2),s) \leftrightarrow \operatorname{At}(x,l_1,s)\land \operatorname{Connected}(l_1,l_2). ]
The formula states that the movement is executable exactly when the object occupies its stated point of departure and the two locations stand in the required static relation.
Successor-state axioms specify how each fluent changes after every relevant action. A representative axiom for location is
[ \begin{aligned} \operatorname{At}(x,l,\operatorname{do}(a,s)) \leftrightarrow {} & a=\operatorname{move}(x,l',l)\ &{}\lor \bigl(\operatorname{At}(x,l,s)\land \neg\exists l'', a=\operatorname{move}(x,l,l'')\bigr). \end{aligned} ]
The first part describes how the fluent becomes true: the action moves (x) into (l). The second part describes persistence: (x) remains at (l) when it was already there and the action does not move it elsewhere. A complete successor-state axiom therefore combines the positive and negative effects affecting one fluent with the conditions under which its previous value persists.
Unique-name axioms distinguish action symbols and their parameterizations. They entail, for example, that a movement action is not identical to an unrelated action and that two movement terms are equal only when their corresponding parameters are equal. These axioms support syntactic reasoning about which action has occurred.
Foundational axioms characterize the structure of situations. They make (S_0) different from every successor situation, ensure that equal successor situations have equal immediate predecessors and final actions, and define the prefix ordering over histories. Together with a second-order induction axiom, they restrict the situation domain to histories generated from (S_0) by finitely many applications of (\operatorname{do}).
Persistence and the frame problem
A direct effects-only description does not state what remains unchanged after an action. Adding a separate frame axiom for every unaffected fluent–action pairing produces a theory whose size grows rapidly with the number of actions and fluents. This representational difficulty constitutes the classical frame problem within action formalisms.
Successor-state axioms address the problem by collecting all conditions that change a given fluent into a single equivalence. Every remaining case inherits the fluent’s preceding value. This method relies on a causal completeness assumption: the theory’s effect conditions exhaust the represented ways in which the fluent changes.
The method does not by itself eliminate the inferential frame problem, which concerns the computational cost of deriving persistent facts. It also remains distinct from the qualification problem, in which an action may have indefinitely many exceptional preconditions, and from the ramification problem, in which direct effects produce indirect consequences through domain constraints.
Regression
Regression transforms a formula about a successor situation into an equivalent formula about its predecessor. When a query contains a fluent whose situation argument has the form (\operatorname{do}(a,s)), the relevant successor-state axiom replaces that occurrence with conditions concerning (a) and (s). Repeated application removes the represented action sequence from the query and reduces the result to a formula about (S_0).
For a fixed action sequence (\alpha) and a query (G), regression yields a formula (\mathcal{R}[G]) satisfying
[ \mathcal{D}\models G(\operatorname{do}(\alpha,S_0)) \quad\text{if and only if}\quad \mathcal{D}{S_0}\cup\mathcal{D}{una}\models\mathcal{R}[G], ]
under the consistency and completeness conditions imposed by the basic action theory. Here (\mathcal{D}{S_0}) denotes the initial-state theory, while (\mathcal{D}{una}) denotes the unique-name axioms for actions.
Regression supports temporal projection, which determines whether a condition follows after a specified action sequence. It also reduces certain executability questions to initial-state reasoning because action precondition axioms are regressed along with fluent formulas. The resulting inference remains within first-order reasoning for the standard regressable fragment, despite the use of second-order foundational axioms in the full semantics.
State equivalence and history identity
Situation calculus distinguishes histories from the states reached through those histories. If two different action sequences produce identical fluent values, the corresponding situations remain unequal unless their final actions and predecessors are identical. This history-sensitive identity permits formulas to describe how a state was reached rather than only which state currently holds.
A derived equivalence relation can identify situations that agree on all relevant fluents:
[ s\equiv_F s' \leftrightarrow \bigwedge_{F\in\mathcal{F}} \forall \bar{x}, \bigl(F(\bar{x},s)\leftrightarrow F(\bar{x},s')\bigr). ]
Such equivalence is weaker than equality between situations. The distinction separates situation calculus from formalisms in which nodes correspond directly to extensional states, including many presentations of transition systems.
Extensions
Nondeterministic actions require a representation in which the agent’s selected action and the environment’s realized outcome are distinguished. One treatment introduces deterministic outcome actions beneath a nondeterministic agent-level action. Reasoning then quantifies over the outcomes compatible with the selected action.
Concurrent versions replace a single atomic action with an action set or with a structured concurrent-action term. Their axioms define when the combined occurrence is executable and how interactions among simultaneous effects alter successor-state conditions.
Epistemic situation calculus adds relations between situations to represent an agent’s uncertainty. An accessibility relation associates the actual history with histories the agent considers possible, while sensing actions eliminate alternatives incompatible with an observation. This construction connects the formalism with epistemic logic.
The high-level programming language GOLOG gives procedural structure to actions described by a situation-calculus theory. Its semantics defines program execution through logical relations over situations, allowing conditionals, iteration, and nondeterministic choice to be interpreted against the same axiomatized action domain.