Editing Frame problem (section)

===Successor state axioms solution===
The value of a condition after the execution of an action can be determined by
the fact that the condition is true if and only if:

# the action makes the condition true; or
# the condition was previously true and the action does not make it false.

A [[successor state axiom]] is a formalization in logic of these two facts. For
example, if <math>\mathrm{opendoor}(t)</math> and <math>\mathrm{closedoor}(t)</math> are two
conditions used to denote that the action executed at time <math>t</math> was
to open or close the door, respectively, the running example is encoded as
follows.

: <math>\neg \mathrm{open}(0)</math>
: <math>\neg \mathrm{on}(0)</math>
: <math>\mathrm{opendoor}(0)</math>
: <math>\forall t . \mathrm{open}(t+1) \iff \mathrm{opendoor}(t) \vee (\mathrm{open}(t) \wedge \neg \mathrm{closedoor}(t))</math>

This solution is centered around the value of conditions, rather than the
effects of actions. In other words, there is an axiom for every condition,
rather than a formula for every action. Preconditions to actions (which are not
present in this example) are formalized by other formulae. The successor state
axioms are used in the variant to the [[situation calculus]] proposed by
[[Ray Reiter]].