4.3.1 Well-Formedness Constraints

Consider a solution tree for a description \phi. Further consider the node \NODE{x}, in that tree, interpreting variable x occurring in \phi. When observed from the vantage point of this node, the nodes of the tree (hence the variables that they interpret) are partitioned into 4 regions: \NODE{x} itself, all nodes above, all nodes below, and all nodes to the side (i.e. in disjoint subtrees).

The variables of \phi are correspondingly partitioned: all variables that are also interpreted by \NODE{x}, all variables interpreted by the nodes above, resp. below or to the side. We introduce 4 variables to denote these sets:

\EQV{x}, \UPV{x}, \DOWNV{x}, \SIDEV{x}

Clearly, x is one of the variables interpreted by \NODE{x}:

x\in \EQV{x}

Furthermore, as described above, these sets must form a partition of the variables occurring in \phi:

\VARS(\phi) = \EQV{x}\uplus\UPV{x}\uplus\DOWNV{x}\uplus\SIDEV{x}

Denys Duchier
Version 1.2.0 (20010221)