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) ≡ ¬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
S₀	—	Initial situation	Starting state
do(a, s)	—	Do	Result of action a in s
Poss(a, s)	—	Possible	Action a possible in s
s ⊏ s'	—	Precedes	s is proper prefix of s'
Holds(f, s)	—	Holds	Fluent f true in s
≺	U+227A	Before	Temporal ordering

Metatheory. Successor state axioms provide a solution to the frame problem in classical logic. Regression is sound and complete for basic action theories. Planning in situation calculus is undecidable in general (reduces to first-order theorem proving). Special cases (STRIPS-like) are decidable. Golog has formal semantics via situation calculus.

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. First-order, so reasoning is undecidable. Continuous time and concurrent actions require extensions. The initial state must be fully specified (or incompletely with epistemic extensions). Scaling to complex domains requires careful axiom engineering. Frame problem "solution" is really a methodology, not automatic. Stochastic actions, partial observability need extensions (DTGolog, PKS).