A problem arises when the well-known stuffy room scenario is formalized with a state constraint that when both vents are blocked by pillows the room is stuffy and changes in fluents are minimized. This can lead to the unintended model that when one vent is already blocked the action of blocking the other event causes the blocked vent to become unblocked in order to minimize change. Some complication of the formalism is required to deal with the phenomenon. Direct formalization in terms of actions and events avoids the difficulty. Also it corresponds better to the way we humans think about the problem, i.e. we think about the room becoming stuffy.
We use fluents , , and . We have the action events , , , and the internal events and .
Effect axioms:
Occurrence axioms:
The frame axioms are
How they work is described in section 6.
We need to distinguish between internal events like Getstuffy and external events like Block1. As we shall see, an external event may be an internal event of a more comprehensive narrative, e.g. one in which Block1 occurs when Mike is annoyed by cold air coming from Vent1.
We can tell a simple sequential story by first describing S0, e.g. by
We can now write the narrative
Here is like the Rr of [McC95]. It is the result of doing a followed by the occurrence of whatever internal events occur. The assumption is that some sequence of internal events will occur after which the situation remains the same until another external event occurs. is undefined in the buzzer example in which internal events occur forever.
requires an induction axiom or schema. Here's one candidate:
The function has the same relation to that Next has to Result. It gives the next situation to which no occurrence assertion applies. satisfies
In the present case we will have
because no internal event will occur in Result(Block1,S0). However, we'll have
because now the internal event Getstuffy will occur. Thus we'll
have but Holds(Stuffy,S2),
,
and
Holds(Stuffy,S4).
We can write
which can also be written
Here we extend the meaning of Result to allow a sequence of events as an argument.