Situation Calculus
Origin. John McCarthy and Patrick Hayes introduced situation calculus (1969) for reasoning about action and change. The frame problem (what doesn't change?) became central. Ray Reiter's solution (1991) using successor state axioms became standard. Foundation for cognitive robotics, planning, and agent programming (Golog).
Models. Actions, situations, and fluents. A situation is a history of actions from an initial state. Fluents are properties that can change (holding(block), location(robot)). Actions transform situations. The challenge: specify what changes and what stays the same (frame problem).
Formalism.
Ontology:
- Situations: histories of actions. S₀ is initial. do(a, s) is result of action a in situation s.
- Actions: terms like move(x, y), pickup(obj), open(door)
- Fluents: predicates or functions that vary with situation
- Relational: Holding(obj, s), On(x, y, s)
- Functional: Location(robot, s) = pos
Basic axioms:
Action precondition axioms: Poss(pickup(x), s) ≡ ¬∃y Holding(y, s) ∧ NextTo(x, s) "Possible to pick up x iff not holding anything and next to x"
Successor state axioms (Reiter's solution to frame problem): Holding(x, do(a, s)) ≡ (a = pickup(x)) ∨ (Holding(x, s) ∧ a ≠ putdown(x)) "Holding x after action a iff just picked it up OR was holding it and didn't put it down"
This solves the frame problem: one axiom per fluent specifies exactly when it changes.
Initial state axioms: Describe S₀ completely.
Foundational axioms:
- Unique names for actions
- do(a₁, s₁) = do(a₂, s₂) → a₁ = a₂ ∧ s₁ = s₂
- Induction over situations
Regression: To determine if φ holds in do(a, s), substitute successor state axioms back to get a formula about s. Reduces queries about future to queries about now.
Planning: Find action sequence a₁, ..., aₙ such that Goal holds in do(aₙ, do(..., do(a₁, S₀)...))
Golog: Programming language over situation calculus:
- Primitive actions
- Sequence, conditionals, loops
- Nondeterministic choice
- Procedures
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊏ | U+228F | Square image of / Precedes | s is a proper prefix of s' in the situation tree |
| ≡ | U+2261 | Biconditional | Form of precondition and successor state axioms |
| ¬ | U+00AC | Negation | Denial in a precondition or effect condition |
| ∧ | U+2227 | Conjunction | Compound precondition |
| ∨ | U+2228 | Disjunction | Positive and persistence cases of a successor state axiom |
| → | U+2192 | Material conditional | Foundational axiom on do-terms |
| ≠ | U+2260 | Inequality | Action distinct from the one that undoes the fluent |
| = | U+003D | Equals sign | Identity of action terms; value of a functional fluent |
| ⊨ | U+22A8 | Double turnstile / Entailment | Consequence from the action theory |
| S₀ | — | Initial situation | The empty history |
| do(a, s) | — | Do | The situation resulting from performing a in s |
| Poss(a, s) | — | Possible | Action a is executable in s |
| Holds(f, s) | — | Holds | Fluent f is true in s |
| R | — | Regression operator | Rewrites a query about do(a, s) into one about s |
| D | — | Basic action theory | Foundational, unique-name, precondition, successor state and initial axioms |
Metatheory. A basic action theory D comprises foundational axioms for the tree of situations — among them a second-order induction axiom — unique-names axioms for actions, one precondition axiom per action, one successor state axiom per fluent, and a description of S₀. Reiter (1991) showed that the successor state axioms are derivable from ordinary effect axioms together with a causal completeness assumption, which replaces one frame axiom per fluent-action pair by one axiom per fluent and keeps the solution inside classical monotonic logic. He also proved the regression theorem: for a regressable sentence W, D ⊨ W if and only if D_S₀ together with the unique-names axioms entails R[W]. Entailment in the full dynamic theory therefore reduces to entailment in the initial database, and regression is sound and complete for such queries. Pirri and Reiter (1999) proved relative satisfiability, so a basic action theory is satisfiable exactly when its initial database is: the dynamics cannot introduce inconsistency by themselves. The dual operation is worse behaved — Lin and Reiter (1997) showed that the progression of an initial database is in general only second-order definable.
Applies to. Cognitive robotics. AI planning. Agent programming. Reasoning about databases (transactions as actions). Game playing. Specifying dynamic systems. Understanding natural language about change.
Limitations. The language is first-order and the foundational induction axiom second-order, so entailment is undecidable and planning is theorem proving; the decidable cases come from restricting to STRIPS-like fragments, not from anything internal to the calculus. Regression applies only to regressable sentences — a ground situation term, no quantification over situations — so a query about whether a goal holds at some unspecified later situation falls outside it, and the alternative route, progression, need not stay first-order. Situations are histories, so the ontology is discrete and strictly sequential: concurrency, continuous change and actions with duration require altering the foundational axioms rather than being definable over them. Successor state axioms presuppose causal completeness, that every way a fluent can change has already been listed, so the frame problem is solved relative to a domain the axiomatizer closed by hand. Ramification and qualification are untouched: indirect effects and unlisted preconditions must be axiomatized separately.
© 2026 Lingenic LLC