Conventional planning literature often speaks of clobbering and achieving preconditions of plans [Weld, 1994]. In CHiPs, these notions are slightly different since inconditions can clobber and be clobbered, as seen in the previous section. Formalizing these concepts and another, undoing postconditions, helps us define summary conditions (in Section 3.2). However, it will be convenient to define first what it means to assert a condition. Figure 5 gives examples of executions involved in these interactions, and we define these terms as follows:
Definition 2 states that an execution in a history asserts a literal at time if that literal is an effect of that holds in the state at . Note that that from this point on, beginning in Definition 3, we use brackets [ ] as a shorthand when defining similar terms and procedures. For example, saying ``[, ] implies [, ]'' means implies , and implies . This shorthand will help us avoid repetition, at the cost of slightly more difficult parsing.
So, an execution achieves or clobbers a precondition if it is the last (or one of the last) to assert the condition or its negation (respectively) before it is required. Likewise, an execution undoes a postcondition if it is the first (or one of the first) to assert the negation of the condition after the condition is asserted. An execution clobbers an incondition or postcondition of if asserts the negation of the condition during or at the end (respectively) of . Achieving effects (inconditions and postconditions) does not make sense for this formalism, so it is not defined. Figure 5 shows different ways an execution achieves, clobbers, and undoes an execution . and point to where they are asserted or required to be met.