Editing Frame problem (section)

===Fluent occlusion solution===
This solution was proposed by [[Erik Sandewall]], who also defined a [[formal language]] for the specification of dynamical domains; therefore, such a domain can be first expressed in this language and then automatically translated into logic. In this article, only the expression in logic is shown, and only in the simplified language with no action names.

The rationale of this solution is to represent not only the value of conditions over time, but also whether they can be affected by the last executed action. The latter is represented by another condition, called occlusion. A condition is said to be ''occluded'' in a given time point if an action has been just executed that makes the condition true or false as an effect. Occlusion can be viewed as “permission to change”: if a condition is occluded, it is relieved from obeying the constraint of inertia.

In the simplified example of the door and the light, occlusion can be formalized by two predicates <math>\mathrm{occludeopen}(t)</math> and <math>\mathrm{occludeon}(t)</math>. The rationale is that a condition can change value only if the corresponding occlusion predicate is true at the next time point. In turn, the occlusion predicate is true only when an action affecting the condition is executed.

:<math>\neg \mathrm{open}(0)</math>
:<math>\neg \mathrm{on}(0)</math>
:<math>\mathrm{open}(1) \wedge \mathrm{occludeopen}(1)</math>
:<math>\forall t . \neg \mathrm{occludeopen}(t) \implies (\mathrm{open}(t-1) \iff \mathrm{open}(t))</math>
:<math>\forall t . \neg \mathrm{occludeon}(t) \implies (\mathrm{on}(t-1) \iff \mathrm{on}(t))</math>

In general, every action making a condition true or false also makes the corresponding occlusion predicate true. In this case, <math>\mathrm{occludeopen}(1)</math> is true, making the antecedent of the fourth formula above false for <math>t=1</math>; therefore, the constraint that <math>\mathrm{open}(t-1) \iff \mathrm{open}(t)</math> does not hold for <math>t=1</math>. Therefore, <math>\mathrm{open}</math> can change value, which is also what is enforced by the third formula.

In order for this condition to work, occlusion predicates have to be true only when they are made true as an effect of an action. This can be achieved either by [[Circumscription (logic)|circumscription]] or by predicate completion. It is worth noticing that occlusion does not necessarily imply a change: for example, executing the action of opening the door when it was already open (in the formalization above) makes the predicate <math>\mathrm{occludeopen}</math> true and makes <math>\mathrm{open}</math> true; however, <math>\mathrm{open}</math> has not changed value, as it was true already.