Proposed change to OWL DL semantics

Further to my earlier emails regarding ontologies that force and empty
universe of discourse. I propose that we augment the definition of an
Abstract OWL interpretation in Section 3 of S&AS with the condition
that EC(owl:Thing) is a non-empty set (we already have that R, the
resources of I, is a non-empty set). This would have the benefit that:

- axioms such as "A implies not A" would be considered inconsistent
(currently this is consistent).

- ontology consistency in OWL DL would be equivalent to the
consistency of the class Thing (using the standard definition of class
consistency);

- an OWL DL ontology would be inconsistent just in case the
corresponding FO theory entails false;

- an OWL DL ontology would be inconsistent just in case the
corresponding SHOIQ(Dn) knowledge base is inconsistent.

Regards, 

Ian