In the situation calculus it is usual to specify the effects of actions by writing effect axioms, like,
If we move to a formalism that allows other events to occur between s and , then this way of specifying change needs to be adjusted. It is possible that something might occur in the time between s and that causes the event to have a different result. For this reason it seems natural to allow the preconditions, those things that hold on the left hand side, to mention properties of all times between s and .
In previous versions of the situation calculus the preconditions for an event were always modeled as a set of fluents, namely those fluents that had to hold at s, for the event to have an effect at . If we allow other things to happen during an event, we cannot just specify the preconditions that must hold at the beginning of the event.
Consider a plane journey from Glasgow to London. It is necessary that the plane be in working order for the entire flight. It is also necessary to be in Glasgow at the beginning of the flight, but clearly, there is no need for this precondition to persist for the entire flight. It is necessary to have a ticket, until the airline steward takes it from you. This is an example of a precondition, ``having a ticket'' that must hold neither just at the moment the event starts, nor for the entire duration.
Consider another example from the Yale Shooting Problem. In order to successfully shoot a person, the gun must be loaded when the trigger is pulled, but the target must remain in the cross-hairs until the bullet hits. We represent the fact the target is in the cross-hairs by aimed. Thus we write:
A possible objection to this example is that if the target arrives in the cross-hairs at any time before impact and remains in the path of the bullet, then they will be killed. In this case we write,
However, both these examples show the need for preconditions to be richer than a statement of what properties hold just when the event occurs. What possible properties can occur as preconditions is important because we wish to know what kinds of axioms can occur as effect axioms.
Before we consider how to represent preconditions, we recall how we represented all possible preconditions earlier. If we wish to introduce a predicate that can parameterize all effect axioms in the old-fashioned situation calculus can write,
following [Cos97]. g is a predicate on fluents that encodes the preconditions. Parameterizing all effect axioms allows us to minimize effect axioms easily.
However, as we want to have preconditions that can extend over the duration of the event, we need more than one set of fluents. For this reason we allow as preconditions, two sets of fluents. The first set need only hold at the start of an event, while the others must persist for the entire event.
It might seem that this does not model preconditions that need hold for only part of the duration of the event. However, we can model these by using other defined fluents. Thus we can write that ``It is necessary to have a ticket, until the airline steward takes it from you.'' using a new fluent defined by
This fluent should hold for the entire duration of the flight. is a shorthand for .
We can write ``It is necessary that the plane be in working order for the entire flight'' using the fluent WorkingOrder,
We can add `` It is necessary to be in Glasgow at the beginning of the flight''
Now that our preconditions are represented as two sets, rather than one, we redefine Changes as follows:
We find it useful to introduce a predicate Succeeds(e,f,s) defined as,
We usually would write a frame axiom for a fluent, say On(A,Top(B)), block A is on the top of block B, and an action, in this case Shoot as,
However, since no longer encodes what events occurred, we need to say something like, ``if no event that could change the fluent On(A,Top(B)) occurred in the interval between s and s' and On(A,Top(B)) held at s then On(A,Top(B)) will hold at s'.'' It is notable that this needs the notion of Changes that we introduced above. Thus we write,
This will generate all of our frame axioms if we minimize Changes, varying Succeeds and , and allowing the domain to vary as in [Cos98b, Cos98a]. We do not consider using non-monotonic reasoning to minimize Changes here, as we wish to stress other issues. Thus we explicitly axiomatize the result of the minimization, much in the same way as Reiter[Rei91] uses an explanation closure axiom and an explicit statement of what events can change what fluents.