- From: Mike Smith <msmith@clarkparsia.com>
- Date: Fri, 16 Jan 2009 10:31:50 -0500
- To: Michael Schneider <schneid@fzi.de>
- Cc: W3C OWL Working Group <public-owl-wg@w3.org>
On Fri, Jan 16, 2009 at 05:49, Michael Schneider <schneid@fzi.de> wrote: > Maybe I am confused (because it's hard to believe), but I think this test case (see [1] for the original version) shows that the famous Theorem 2 of OWL (given in [2]) was actually wrong: It is /not/ the case that every OWL DL entailment is an OWL Full entailment. This is big news (at least to me; apparently not to Jeremy, who originally wrote this test case :-))! No, I don't believe so. The test was approved as a non-entailment -- there is no entailment in this case that disproves the theorem. > According to its description, the test case is about a weakness of the OWL Full comprehension principles. While this is kind of interesting (since the main purpose of the comprehension principles was to make Theorem 2 true), the problem does not really depend on the comprehension principles. Below, I have created a much simpler test case that shows the core of the problem. > > Consider the RDF graph > > G := { > ex:c rdf:type owl:Class . > ex:c rdfs:subClassOf owl:Thing . > } > > This is a valid OWL (2) DL ontology in RDF graph form, and it reverse-maps to the Functional Syntax ontology > > F(G) = { > Declaration(Class(ex:c)) > SubClassOf(ex:c owl:Thing)) > } > > AFAICT (please confirm!), under the OWL 2 Direct Semantics F(G) can be entailed from the empty ontology, i.e. every interpretation of the vocabulary used in F(G) is a model for F(G). (FIXME: Is this also the case under the OWL 1 Direct Semantics and with the OWL 1 Abstract Syntax?) I agree with that this can be entailed from the empty ontology using the OWL 2 direct semantics. > But under the OWL (2) Full Semantics, not every interpretation of the vocabulary used in G is also a model for G, since the name ex:c does not always need to denote a class. So there exist OWL (2) Full interpretations by which the first triple is unsatisfied. Hence, G is not entailed by the empty OWL (2) Full ontology. And so Theorem 2 does not hold. > > I do not see a way to adjust the original comprehension principles to cope with this problem. However, I can see how to extend my new notion of "entailment balancing" (see [3]), because I can additionally copy all typing triples, which are reverse-mapped to declarations, from the right hand side of an entailment to the left hand side. With this, it will then (hopefully finally) be true that every OWL 2 DL entailment is also an OWL 2 Full entailment, modulo some simple direct-semantics preserving transformation that I now call "OWL 2 balancing". > > With other words, the test case in [1] could then be regarded as a /positive/ entailment test not only for OWL 2 DL, but also for OWL 2 Full. (For this to hold, the test case still needs to be "OWL 2 balanced", which can be done by an automatic syntactic preprocessing step that does not change the semantic meaning of the test case w.r.t. the OWL 2 Direct Semantics). An alternative might be to constrain the definition of V in the direct semantics such that the test remains a non-entailment and the empty ontology does not entail the ontology you provide above. -- Mike Smith Clark & Parsia
Received on Friday, 16 January 2009 15:32:30 UTC