RE: The definition of entailment in the Direct Semantics document

>-----Original Message-----
>From: public-owl-wg-request@w3.org [mailto:public-owl-wg-request@w3.org]
>On Behalf Of Mike Smith
>Sent: Friday, January 16, 2009 4:32 PM
>To: Michael Schneider
>Cc: W3C OWL Working Group
>Subject: Re: The definition of entailment in the Direct Semantics
>document
>
>
>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.

I think that this is primarily a non-entailment test for OWL /Full/! See the
description of the test:

  "This test shows a potential misapplication of 
  OWL Full comprehension rules."

Ok, I can see that in the upper left corner, it is marked as a test for "DL
Full". I guess that's a typo. Because I can also see that there is this
typing triple with rdfs:Class. That's a bit strange, but is in my eyes
another hint that this is only a test for OWL Full, not for OWL DL.

 (I always forget about these allowed situations in that rdfs:Class may
occur in an OWL DL ontology, and in OWL 2 DL this is, AFAIR, also allowed
sometimes. But in general, one should assume that an entailment test that
refers to rdfs:Class is only meant to be an OWL /Full/ entailment test,
since in many cases such an entailment query would not even be syntactically
valid in OWL (2) DL).

>> 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.

Why? I would say that this really SHOULD be an entailment under the OWL 2
Direct Semantics, no?

Before I would go and change the OWL 2 Semantics significantly, I would
rather consider the possibility that this particular test case might simply
be wrongly marked as a DL non-entailment test... 

And we can also simply decide to drop this test case completely, since we
are not perfectly clear about its intended purpose and its correctness.
Anyway, it is about OWL Full comprehension principles, and there are no
comprehension principles in the normative part of OWL 2 Full anymore, so the
test case seems moot to me.

Michael