Class definitions

A class definition is either a pair $\langle \ensuremath{\textsf{CN}},D \rangle$ or a triple $\langle \ensuremath{\textsf{CN}},P,D \rangle$, where $\textsf{CN}$ is a class name, $D$ is a class description and $P$ is either primitive or defined; $\langle \ensuremath{\textsf{CN}},D \rangle$ is equivalent to $\langle \ensuremath{\textsf{CN}},\key{primitive},D \rangle$. A class definition $\langle \ensuremath{\textsf{CN}},\key{primitive},D \rangle$ is written $\ensuremath{\textsf{CN}} \sqsubseteq D$ (it states that $\textsf{CN}$ is a subclass of the class described by $D$) and a class definition $\langle \ensuremath{\textsf{CN}},\key{defined},D \rangle$ is written $\ensuremath{\textsf{CN}} \doteq D$ (it states that $\textsf{CN}$ is equivalent to the class described by $D$).

A class description $D$ consists of an optional subclass-ofcomponent, itself a list of one or more class-expressions $C_1,\ldots,C_n$, followed by a list of zero or more slot-constraints $A_1,\ldots,A_m$. We will write such a class description as

$$[C_1,\ldots,C_n,A_1,\ldots,A_m].$$