during the seeding process. Therefore, the maximum number of occurrences of a property p in Ps, possessed by any object in Os in any state of the world, will be bounded by the maximum number of instances of that property in any state in Ss (these maximum values might not be equal since Ss can contain inaccessible states). The identity invariants simply express this bound on the properties of the objects in Os.

Every object in Os must be in a state in Ssind Ssubs. This follows by definition of these sets in Definition 16 and by Theorem 1. The state membership invariants assert that ery object in Os must be in at least one of these states, with each disjunct in the invariant corresponding to the assertion of membership of one of these states.

To argue for the correctness of the unique state invariants, we observe that the proposed invariants would only be false if they paired states that were not mutually exclusive. In this case, either the state extension process would have put properties that could be simultaneously held into the same bag, or such properties would be simultaneously held in the initial state and hence would appear in the same bag on initial construction of the property space. In either case, a state will exist in the property space that is a superset of both of the non-exclusive states. However, uniqueness invanants are generated for pairs of states drawn only from S sind S sups so these non-exclusive pairs of states will not lead to the generation of incorrect invariants.

口 The fixed resource invariants are always associated with a particular predicate. If atoms built with that predicate are balanced on the add and delete lists of all of the operator schemas then the number of occurrences of these atoms in the initial state is fixed over all ssssssssss every predicate that forms balanced atoms.

Since no new techniques are required to infer invariants from sub-spaces, no further argument is required to support correctness of the invariants formed following sub-space analysis.

Although Theorem 2 demonstrates the correctness of the invariants inferred by tim it is possible for weak invariants to be inferred from the presence of unreachable states in Ss.

Weakidentity invariants are inferred if an unreachable state is generated, during extension, containing more instances of a property than are contained in any reachable state. When this happens an identity invariant will be generated that is weakerthan would be ideal, but is still valid. Further, if a property space contains unreachable states they will cause the inclusion of additional false disjuncts in the state membership invariants, but since these false disjuncts will not exclude satisfying assignments their presence will not invalidate the invariants. Unreachable states cause additional tautologous uniqueness invariants to be generated but do not affect the strength of the invariants that refer only to reachable states. Clearly we cannot hope to identify all of the unreachable states, as such an analysis would be as hard as planning itself.

Because no invariants are generated for attribute spaces tim cannot be claimed to be complete. Sub-space analysis rectifies this to some extent by identifying property spaces that exist within attribute spaces and allowing further invariants to be generated. This analysis could be further refined.