Soundness

[Chapman 87] discusses precondition ``clobbering'', the state where a rule that had been instantiated previously on the basis of some precondition, later had that precondition removed, invalidating the rule. Many previous text planners were not ``sound'', in that they did not detect this kind of situation. To prove more formally that this system is sound, let me state the soundness criterion which it claims to adhere to:

Soundness Criterion: At all times, every rule that is not marked as currently failed must, for each of its preconditions, have at least one active, non-failed plan that has an effect that satisfies the precondition if it is a positive constraint (i.e. some state must exist for the precondition to be satisfied, identified by a ``check-con'' in the precondition field), or have no plans active that have an effect equal to the precondition if it is a negative constraint (i.e. the state may not exist, identified by a ``check-not-con'').

Thus, if plan 1 has a precondition that states that constraint A must be true, then whenever plan 1 is not marked failed, there must be at least one other active plan that has an effect that produces A. On the other hand, if plan 1 has a precondition that states that precondition B must not be true, then there can be no plans active that produce B while rule 1 is not failed.

Note that this is slightly stronger than a general soundness condition, which might allow a planner to go through unsound states as long as the final result is sound. These ``non-monotonic'' plans, though valid, are currently excluded by HUNTER-GATHERER. We do not feel that this is a big drawback, since, in practice, a planner that is guaranteed to be sound at the end most likely will be sound throughout. This is all the more true for computational semantic planners which do not have complex preconditions and effects.

This system meets the soundness criterion given above. After some basic precondition application, which removes any rules that do not meet unary constraints (for example, ``only apply this rule in formal contexts''), the dependencies between all the remaining rules are analyzed. The following information is recorded:

1. for each precondition of each plan, the plans are recorded that, if instantiated, would produce constraints that conflict with the precondition

2. the inverse of the above: for each plan, if it were instantiated, record all the preconditions that conflict with it.

3. for each precondition that requires a constraint A, record all of the plans that, if instantiated, would set constraint A.

4. the inverse of the above: for every plan, if it were instantiated, record all the preconditions that would be satisfied by it.

Before solution synthesis is initiated, every plan that has a precondition for which there were no plans found in number 3 above is failed. Every time a plan is failed, both during this initial process and during the subsequent syntheses, all of the preconditions it can satisfy (from number 4 above) are retrieved. For each of these preconditions, all of the plans that could satisfy the precondition (from number 3 above) are retrieved, and it is checked that at least one of these plans is still active. If none are, then the plan corresponding to the precondition is failed. This process ensures that no plans are ever deleted that are the sole suppliers of preconditions of other active plans (or more accurately, that any such active plans are failed if their sole supplier is failed).

This does not yet fail preconditions that conflict with constraints. Whenever a variable has only one valid plan left, all of the preconditions that conflict with the plan (from number 2 above) are retrieved and the corresponding plan(s) are failed. The plans affected by these failures are then checked as described above.

During the solution synthesis, valid combinations of plans are chosen for each variable in the synthesis. In a combination, each variable has one plan chosen and the others are failed. The effects of failing the other plans are checked, and the effects of instantiating the plan that is used are checked. In general, whenever a plan is failed, the plans for which it supplied preconditions are checked. Whenever an island is created, the plans that conflict with the island are failed.

The fact that the system is sound is good in itself. But this is not where the benefits end. The whole process of ensuring soundness as described above, combined with island processing, creates a very efficient text planner. All conflicting rules and impossible rules are eliminated at the earliest point possible. Circles are created for the solution synthesizer that will maximize this effect. A plan is not ever failed, and then, after further processing, a different plan found to be invalid as a result. As soon as a plan is failed or an island created, all the other plans that can no longer be valid are removed immediately. Removing these plans then may lead to further removals by the same process. This process feeds on itself to remove as many of the possible plans as possible.