Fluent Calculus

Origin. Thielscher developed Fluent Calculus (1999). Evolution of Situation Calculus. States as explicit objects containing fluents. Addresses frame problem via state update axioms. Foundation for FLUX agent programming system.

Models. States as first-class citizens. Situation Calculus: fluents hold in situations. Fluent Calculus: states contain fluent collections. State update: add/remove fluents explicitly. Avoids frame axioms by manipulating state terms.

Formalism.

State terms: States built from fluents using ∘ (composition) and ∅ (empty). state = ∅ | f | state ∘ state

Example: On(a,b) ∘ On(b,c) ∘ OnTable(c)

Holds predicate: Holds(f, s): fluent f is in state s. Defined equationally via state structure.

State update axioms: State(Do(a, s)) = s - Effects⁻(a) + Effects⁺(a) Explicitly computes new state from old.

Example — blocks world: State(Do(Move(x,y,z), s)) = s - On(x,y) + On(x,z) Moving x from y to z: remove On(x,y), add On(x,z).

Foundational axioms:

∅ ∘ s = s
s₁ ∘ s₂ = s₂ ∘ s₁
(s₁ ∘ s₂) ∘ s₃ = s₁ ∘ (s₂ ∘ s₃)
Holds(f, s₁ ∘ s₂) ↔ Holds(f, s₁) ∨ Holds(f, s₂)

Regression: Reason backwards from goal to initial state. Efficient for planning.

Symbols.

Symbol	Unicode	Name	Meaning
∘	U+2218	Ring operator / State composition	Associative and commutative merge of state terms
∅	U+2205	Empty set	The empty state, unit for ∘
↔	U+2194	Biconditional	Definition of Holds over a composed state
∨	U+2228	Disjunction	Fluent lies in one component or the other
=	U+003D	Equals sign	Identity of state terms, modulo the foundational axioms
+	U+002B	Plus sign	Adds the positive effects to a state term
-	U+002D	Hyphen-minus	Removes the negative effects from a state term
⁺	U+207A	Superscript plus	Marks the positive effects of an action
⁻	U+207B	Superscript minus	Marks the negative effects of an action
\|	U+007C	Vertical line	Alternation in the grammar of state terms
Holds	—	Containment	Fluent f occurs in state s
Do	—	Do	The situation resulting from performing an action
State	—	State function	The state term associated with a situation
f	—	Fluent	Atomic component of a state term
s	—	State term	Collection of fluents built with ∘

Metatheory. The foundational axioms make ∘ associative and commutative with ∅ as unit, so state terms live in an AC1 equational theory and deciding whether two of them denote the same state is unification modulo AC1: decidable, NP-hard, and finitary, in that a solvable problem has finitely many most general unifiers. The equational encoding of states goes back to Hölldobler and Schneeberger (1990); Thielscher's contribution was to identify what it adds. Reiter's successor state axioms already answer the representational frame problem, but regression must still reason about every fluent at every step, and this is the inferential frame problem: a state update axiom instead rewrites one state term into another by deleting the negative and adding the positive effects, so the cost of a step is the size of the effects rather than the size of the domain. The fluent calculus therefore adds progression as a primitive operation alongside regression. Incomplete initial knowledge is expressed by leaving a state variable in the term under constraints, and FLUX implements this by constraint logic programming.

Applies to. Agent programming. Robotics. Planning. Game AI. Cognitive architectures. Knowledge representation.

Limitations. Reasoning about state terms is unification modulo an associative-commutative theory with unit, which is NP-hard, so what the calculus achieves is a change in what the cost depends on rather than its removal. Subtraction is defined only where the negative effects actually hold, so the single equation State(Do(a, s)) = s - Effects⁻(a) + Effects⁺(a) covers unconditional actions only; context-dependent and conditional effects require case-splitting into several update axioms. A state term is a collection of positive fluents and says nothing about what is false, so either a closed-world reading must be imposed or a state variable carried under constraints, and quantifying over such variables leaves the decidable equational fragment. Actions remain discrete and sequential; duration, concurrency and continuous change are not in the ontology. Ramification is untouched, so indirect effects must be written into the update axioms by hand, exactly as in the formalisms the calculus was meant to improve on.