example, given the subset states at1 and in1 and the superset state at1,in1 ,it can be observed that the two subset states are not mutually exclusive since at1 and in1 can be ssee the state of the state of the state of the state of the state of the state of the state of the state of the state of the state.

of states we mark the subset states as unusable for generation of invariants. The remaining states are considered in all possible painngs. For every pair of states, P,Q, we generate an invariant of the following form assuming, for simplicity, that x is in the first position in Pl Pm and Q 1 ..Qm. The form of the invariant is easily generalised, as before.

$$\begin{array}{l l l l l l}{{x.}}&{{\left(\begin{array}{l l l l l}{{\bar{y}_{1}\dots\bar{y}_{n}.\left(P^{1}\left(x,\,\bar{y}_{1}\right)}&{P^{2}\left(x,\,\bar{y}_{2}\right)}&{\dots}&{P^{n}\left(x,\,\bar{y}_{n}\right)\right)}}\\ {{}}&{{\left(\begin{array}{l l l l l}{{\bar{y}_{1}\dots\bar{y}_{m}.\left(Q^{1}\left(x,\,\bar{y}_{1}\right)}&{Q^{2}\left(x,\,\bar{y}_{2}\right)}&{\dots}&{Q^{m}\left(x,\,\bar{y}_{m}\right)\right)\right)}}\end{array}\right)}}\end{array}$$

The fourth kind of invariant can be inferred from the structure of the operator schemas wit ho ut reference to the property spaces or domain type structure. We call these invanants fixed resource invariants since they capture the physical limitations of the domain. Fixed resource invariants cannot be inferred from the state and attribute spaces because they describe properties of the domain rather than of objects within it. The following schema from the Gripper domain provides an example of why fixed resource invariants are distinguished from the other three kinds:

| move( X,Y)   |                       |
|--------------|-----------------------|
| Pre:         | at_robot(X),  room(Y) |
| Ad:          | at_robot(Y)           |
| Del:         | at_robot(X)           |

The PRSs that would be built from this operator are:
precs :
at_robot 1

| precs :         | at_robot 1   |
|-----------------|--------------|
| deleted_precs : | at_robot 1   |
| add_elements :  |              |

| precs :         |
|-----------------|
| deleted_precs : |
| add_elements :  |

$$r\,o o m_{1}$$  $$a t_{\blacksquare}r\,o b o t_{1}$$

and the rules constructed from these are:

$$a t_{\underline{{{r}}}}\,r o b o t_{1}$$
$$n\,u\,l l$$

and

$$r\,o o m_{1}\qquad n\,u l\,l$$
$$a t_{\underline{{{J}}}}r o b o t_{\mathrm{{P}}}$$

It can be observed that both of these rules are attribute transition rules and that at_robot1 is attribute rather than state-valued. This means that no invariants of the first three kinds discussed would be constructed.

The reason for the lack of invariants of the first three forms is that the encoding of the robot is embedded in a predicate, so the robot cannot participate directly in state transitions. An obvious invariant of the robot, which would naturally be true of this domain, is that the