Situation Calculus

A simple approach to capture information about situations is situation calculus. It is due to John McCarthy and Pat Hayessitcalc. In situation calculus, the world consists of a series of snapshots, situations. Every situation is created from the previous by a series of actions. Relations and properties are noted with a separate situation argument.

$$R(x_1,...,x_n,S_0)$$

Properties subject to change are called fluents.

Changes from one situation to another are modeled using a function, $Result:Action\times Situation \mapsto Situation$. The atomic predicate $Holds(f,S)$ is true, if the fluent $f$ is true in the situation $S$.

Actions are described by stating their effects. Therefore effect axioms have to be stated, describing the properties of a situation that results from doing some action. However, this is not enough. One also has to state axioms describing a situation after not performing an action. Those are called frame axioms. Frame axioms have to be stated for every fluent and action. Another solution is to use a successor-state axiom. This axioms states, that a fluent is true after some action, if an action made it true or it has been true and no action made it false.

This is a very weak theory of situations. The world consists of a series of snapshots, that are complete on its own. There is no development within a situation, since they do not have a duration. We shall therefore turn our attention to a more complex theory of situations.

But first, let us consider an example. We want to open a bottle of beer, smell the beer and after that we drink the beer. So the fluents we have to consider are $closed(x)$ and $empty(x)$, the actions will be $Open$ and $Drink$.

We start off with the beer closed and not empty.

$$Holds(closed(beer),S_0)$$

$$\neg Holds(empty(beer),S_0)$$

Now we want to perform the action of opening the beer, ending up in a new situation.

$$S_1 = Result(Open(beer),S_0)$$

However, this does not do anything yet. We have to put some knowledge about our $Open$ action in our theory, our first effect axiom.

$$\forall x,S (Holds(closed(x),S) \rightarrow \neg Holds(closed(x),Result(Open(x),S)))$$

Now

$$\neg Holds(closed(beer),S_1)$$

is true and our beer is no longer closed. But before consuming the beer we would like to smell it first, because we are in another country and do not trust their ability to brew beer after German purity law.

$$S_2 = Result(Smell,S_1)$$

There is no fluent changed here, because the smelling is rather a symbolic act, we cannot smell the ingredients anyway.

After we finished this ritual, we finally want to drink the beer, ending up in a new situation.

$$S_3 = Result(Drink(beer),S_2)$$

We need some effect axioms too. We can only drink an open, not empty beer. And after we finished drinking, the beer is empty.

$$\begin{split}\forall x,S (\neg Holds(closed(x),S)\land \neg H... ...) \rightarrow\ Holds(empty(x),Result(Drink(x),S))) \end{split}$$

Now the question is, if

$$Holds(empty(beer),S_3)$$

is true. Oddly, it is not. Since there is no axiom saying otherwise, the beer could have closed itself while we were smelling the beer. The beer could have been closed already in $S_2$. Even worse, the beer could have emptied itself at any time! We have to add some frame axioms about things, that do not change, if some action is done. If the beer is empty or open, then there is no way to undo this.

$$\forall a,x,S \left(Holds(empty(x),S)\rightarrow Holds(empty(x),Result(a,S))\right)$$

$$\forall a,x,S \left(\neg Holds(closed(x),S)\rightarrow \neg Holds(closed(x),Result(a,S))\right)$$

Now we have to state, that the bottle only open when we open it, and, more important, that the only way it will get empty is, when we consume it.

$$\forall a,x,S \left( Holds(closed(x),S)\land a\not= Open \rightarrow Holds(closed(x),Result(a,S))\right)$$

$$\forall a,x,S \left( \neg Holds(empty(x),S)\land a\not= Drink \rightarrow \neg Holds(empty(x),Result(a,S))\right)$$

Now our beer will be empty in $S_3$, but not before that.