A minor bug in OWL 2 RL - Theorem PR1

• From: Boris Motik <boris.motik@comlab.ox.ac.uk>
• Date: Mon, 19 Jan 2009 21:07:32 -0000
• To: "'W3C OWL Working Group'" <public-owl-wg@w3.org>
• Message-ID: <214F4700A13240F383BB00FDABF62237@wolf>

Hello,

After having a discussion with Zhe about OWL 2 RL, I noticed that Theorem PR1 in the Profiles document contains a small error: for
the theorem to hold, the entailed ontology should not contain DifferentInfividuals. This minor oversight is demonstrated by the fact
that the ontology

A(a)
B(b)
DisjointClasses( A B )

entails

Differentindividuals( a b )

under the DirectSemantics; however, the OWL 2 RL/RDF rules do not entail the triple

<a, owl:differentIndividuals, b>.

The bug was in that DifferentIndividuals involves negation, but the OWL 2 RL/RDF rules preserve only the positive facts. We can fix
this by deleting DifferentIndividuals from the list of allowed assertions in the entailed ontology. This change obviously does not
impact the implementations; therefore, I believe we can just fix this bug in the Wiki without too much trouble. Please let me know
if you object to this.

Regards,

	Boris

Received on Monday, 19 January 2009 21:08:19 UTC