situations as a result of various actions being performed within the world. A situation represents a history of action occurrences. 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: A situation is a finite sequence of actions. Period. It's not a state, it's not a snapshot, it's a history. The situation before any actions have been performed is typically denoted and called the initial situation. The new situation resulting from the performance of an action is denoted using the function symbol (Some other references also use ). This function symbol has a situation and an action as arguments, and a situation as a result, the latter being the situation that results from performing the given action in the given situation. The fact that situations are sequences of actions and not states is enforced by an axiom stating that is equal to if and only if and . This condition makes no sense if situations were states, as two different actions executed in two different states can result in the same state. In the example robot world, if the robot's first action is to move to location , the first action is and the resulting situation is . If its next action is to pick up the ball, the resulting situation is . Situations terms like and denote the sequences of executed actions, and not the description of the state that result from execution. Fluents Statements whose truth value may change are modeled by relational fluents, predicates which take a situation as their final argument. Also possible are functional fluents, functions which take a situation as their final argument and return a situation-dependent value. Fluents may be thought of as "properties of the world"'. In the example, the fluent can be used to indicate that the robot is carrying a particular object in a particular situation. If the robot initially carries nothing, is false while is true. The location of the robot can be modeled using a functional fluent which returns the location of the robot in a particular situation. Formulae The description of a dynamic world is encoded in second order logics using three kinds of formulae: formulae about actions (preconditions and effects), formulae about