ISSUE-148 (datatype extensibility): owl:topDataProperty may invalidate Theorem 1 from Direct Semantics

ISSUE-148 (datatype extensibility): owl:topDataProperty may invalidate Theorem 1 from Direct Semantics

http://www.w3.org/2007/OWL/tracker/issues/148

Raised by: Boris Motik
On product: 

The addition of owl:topDataProperty causes problems for Theorem 1 in the Direct Semantics document. This theorem says that the semantics of OWL 2 ontologies does not change if the set of built-in datatypes is extended. This, however, may not be true on a logic that provides for both owl:topDataProperty and UnionOf on data ranges. Consider the following axiom:

ClassAssertion(
  AllValuesOf( owl:topDataProperty
    UnionOf( xsd:string xsd:integer ... <add all OWL 2 datatypes> )
  )
  my:individual
)

This axiom says that the only datatypes are the ones currently defined in OWL 2. Thus, the axiom is satisfiable at the moment; however, if the set of OWL 2 datatypes were extended (e.g., in OWL 3), the axiom would become unsatisfiable. It is worth noting that the current situation is OK, but this is mainly because we don't have UnionOf on data ranges: because of that, we cannot write axioms of the above form.

To summarize, by adding owl:topDataProperty to OWL 2, we are restricting all future revisions of OWL 2 either not to provide new datatypes or not to provide UnionOf on data ranges.

My proposal is to remove owl:topDataProperty from the language, or at least to disallow its usage in restrictions.

Received on Sunday, 19 October 2008 15:47:12 UTC