Re: empty Thing (was Re: proposal to approve tests)

On Wed, 2003-10-29 at 17:37, Ian Horrocks wrote:
> The case where an ontology forces Thing to be empty is clearly a
> special case, and we have to decide whether such an ontology should be
> considered consistent. There are good reasons why it should NOT be
> considered consistent (the standard treatment in DL and FOL):
> - If such an ontology is consistent, then the axiom A implies not A is
> consistent.
> - If such an ontology is consistent, then we can have a situation
> where all classes, including Thing, are inconsistent, yet the ontology
> is still consistent (unfortunately we don't explicitly state in our
> documents what it means for a class to be consistent w.r.t. an
> ontology, but the standard definition is that there is some model of
> the ontology in which the class has a non-empty extension).

That seems fairly relevant to real-world use of OWL.

Good enough for me.

I second the proposal to require that OWL DL interpretations
have non-empty universes.

> - If such an ontology is viewed as a FO theory, then the theory
> entails false.
> - If such an ontology is viewed as a DL knowledge base, then the KB is
> inconsistent.
> If we want such ontologies to be considered inconsistent, as I am
> arguing, then the easiest (and standard) way is simply to change the
> definition of what constitutes a model (by insisting that the universe
> be non-empty). This would involve minimal changes to the S&AS document
> and a change to one test case.
Dan Connolly, W3C

Received on Wednesday, 29 October 2003 18:56:27 UTC