Editing Frame problem (section)

===Predicate completion solution===
This encoding is similar to the fluent occlusion solution, but the additional predicates denote change, not permission to change. For example, <math>\mathrm{changeopen}(t)</math> represents the fact that the predicate <math>\mathrm{open}</math> will change from time <math>t</math> to <math>t+1</math>. As a result, a predicate changes if and only if the corresponding change predicate is true. An action results in a change if and only if it makes true a condition that was previously false or vice versa.

:<math>\neg \mathrm{open}(0)</math>
:<math>\neg \mathrm{on}(0)</math>
:<math>\neg \mathrm{open}(0) \implies \mathrm{changeopen}(0)</math>
:<math>\forall t. \mathrm{changeopen}(t) \iff (\neg \mathrm{open}(t) \iff \mathrm{open}(t+1))</math>
:<math>\forall t. \mathrm{changeon}(t) \iff (\neg \mathrm{on}(t) \iff \mathrm{on}(t+1))</math>

The third formula is a different way of saying that opening the door causes the door to be opened. Precisely, it states that opening the door changes the state of the door if it had been previously closed. The last two conditions state that a condition changes value at time <math>t</math> if and only if the corresponding change predicate is true at time <math>t</math>. To complete the solution, the time points in which the change predicates are true have to be as few as possible, and this can be done by applying predicate completion to the rules specifying the effects of actions.