schema are considered, because any object that can satisfy the preconditions of an operator can have the properties represented by the postconditions and is therefore of the right type for instantiation of the operator. When a type is associated with the vector the union of all of its sub-types is taken. This union is then the type assigned to the variable. Any domain object, the type of which is a sub-type of the type associated with the variable, can then be used to instantiate that variable. To see how this process works, consider the variable X
in the drive schema above. The precondition properties of X are: at 1 , fuelled 1 . These are members of the two property spaces 1 and 2. Therefore, the type vector associated with X
is 1100. It can be observed that the type vector associated with the rocket is 1101, so that the type of rocket is a sub-type of the type of X . This is the only sub-type, so the union of sub-types contains only T n , the type of rocket. This means that X can be instantiated by rocket, but not by any other domain constant, since no other domain constant has a type in the appropriate sub-type relation. To type the operator parameters we introduce new type variables, T k . T n for unused values between k and n, where k is the number of existing types and n is k plus the number of variables in the schema being considered.  The type vector for variable Y will be 0010 and Z will have no type vector because location is a static relation and Z does not appear as an argument to any other predicate in the preconditions.

Z therefore acquires the same type as London and Paris, the only two objects for which location is true in the initial state. T 4 is a super-type of T 2 . After taking the unions of the sub-types we can now specify the drive schema in the following way:
drive( X,Y,Z)

$$\begin{array}{l l}{{T_{1},T_{2},T_{3},T_{4},T_{5}}}\\ {{\mathrm{ams:}}}&{{\mathrm{~X:}T_{0}\quad\mathrm{Y:}T_{2}\quad\mathrm{Z:}T_{2}}}\\ {{}}&{{\mathrm{~at\,}(\mathrm{X,Y}),\quad\mathrm{f u e l l e d\,(X\,),\quad l o c a t i o n\,(Z\,)}}}\\ {{\mathrm{:}}}&{{\mathrm{~at\,}(\mathrm{X,Z}),\quad\mathrm{u n f u e l l e d\,(X\,)}}}\\ {{}}&{{\mathrm{~at\,}(\mathrm{X,Y}),\quad\mathrm{f u e l l e d\,(X\,)}}}\end{array}$$

STAN exploits the sub-typing relations that have been inferred when constructing instances of the drive operator. Any variable that appears in a schema but does not appear in its preconditions can be instantiated by objects of any type. This is because the domain description contains no basis for inferring type restrictions in this case. No variable can appear on the delete list without appearing on the precondition list, since we assume that al delete list elements appear as preconditions. So such a variable would have to occur on the add list. This would mean that, regardless of the properties holding of the object used to instantiate that variable, in the initial state, it can acquire that add list property freely. Since this acquisition would occur irrespective of the type of the object, such variables are essentially polymorphic.

## 2.7  The Inference Of State Invariants

The final phase of the computation of TIM is the inference of the state invariants from the property spaces. The attribute spaces are not used for the inference of invanants:
incorrect invariants would be proposed by TIM if attribute spaces were inadvertantly used.

This explains the importance of identifying the attribute spaces in the earlier stages of the agorithm.

The current version of TIM is capable of inferring four kinds of invariant, three of which are inferred from the property spaces (identity invariants, state membership invariants and