Ambiguity in description of DisjointClasses axiom

To whom in may concern,

 I think the description of the DisjointClasses axiom may need
revising.  The informal description states:

9.1.3 Disjoint Classes

A disjoint classes axiom DisjointClasses( CE1 ... CEn ) states that
all of the class expressions CEi, 1 ≤ i ≤ n, are pairwise disjoint;
that is, no individual can be at the same time an instance of both CEi
and CEj for i ≠ j.

The "CEi, 1 ≤ i ≤ n" suggests that an axiom of the form
"DisjointClasses( CE1)" is legal.

However, the formal grammar for DisjointClasses axioms is:

DisjointClasses := 'DisjointClasses' '(' axiomAnnotations
ClassExpression ClassExpression { ClassExpression } ')'

And this clearly makes it clear that at least two ClassExpressions
should be in a DisjointClasses axiom.  There is a bit of confusion,
here, though.  Since axiomAnnotations are optional, one may also
assume that the second ClassExpression axiom is optional (especially
in the light of the "CEi, 1 ≤ i ≤ n" description above).

I suggest that you modify the informal description to read something like:

....  DisjointClasses( CE1 CEi... CEn ) states that all of the class
expressions CEi, 1 ≤ i ≤ n ...

I hope this suggestion is helpful,
Bill

Received on Tuesday, 8 November 2011 12:23:54 UTC