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.


> 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