ISSUE-148

datatype extensibility

RESOLVED: owl:topDataProperty may invalidate Theorem 1 from Direct Semantics

State:

CLOSED

Product:

Raised by:

Boris Motik

Opened on:

2008-10-19

Description:

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.

Related Actions Items:

No related actions

Related emails:

1. Resolution of ISSUE-148 (topDataProperty) implemented (from boris.motik@comlab.ox.ac.uk on 2008-11-07)
2. ISSUE-148 (datatype extensibility): owl:topDataProperty may invalidate Theorem 1 from Direct Semantics (from sysbot+tracker@w3.org on 2008-10-19)

Related notes:

Display change log