RE: The definition of entailment in the Direct Semantics document

Hi!

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 :-))!

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

Cheers,
Michael

[1] <http://www.w3.org/TR/owl-test/XXL#approvedFunction-Class005>
[2] <http://www.w3.org/TR/owl-semantics/rdfs.html#theorem-2>
[3] <http://lists.w3.org/Archives/Public/public-owl-wg/2009Jan/0007.html>

>-----Original Message-----
>From: public-owl-wg-request@w3.org [mailto:public-owl-wg-request@w3.org]
>On Behalf Of Mike Smith
>Sent: Thursday, January 15, 2009 4:29 PM
>To: W3C OWL Working Group
>Subject: The definition of entailment in the Direct Semantics document
>
>
>OWL WG,
>
>I believe, after review of test case [WebOnt-Class-005], that the
>definition of entailment [1] in the OWL 2 Direct Semantics document
>differs from the definition used by the WebOnt WG.  The entailment
>test case is repeated below.  In WebOnt, this was a negative
>entailment test (i.e., O did not entail O').  I believe that with the
>current definitions, it would be a positive entailment test.   If the
>group agrees with this analysis, we can accept the change in
>definition or tweak the Direct Semantics document to match the
>previous (WebOnt) meaning.
>
>O:
> ClassAssertion( owl:Thing x )
>
>O':
> Declaration( Class( C ) )
> ClassAssertion( UnionOf( C ComplementOf( C ) ) x )
>
>--
>Mike Smith
>
>Clark & Parsia
>
>[1] http://www.w3.org/2007/OWL/wiki/Direct_Semantics#Inference_Problems
>[WebOnt-Class-005]
>http://km.aifb.uni-
>karlsruhe.de/projects/owltests/index.php/TestCase:WebOnt-Class-005

--
Dipl.-Inform. Michael Schneider
Research Scientist, Dept. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: schneid@fzi.de
WWW  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555

==============================================================================

FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Stiftung Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Prof. Dr.-Ing. Rüdiger Dillmann, Dipl. Wi.-Ing. Michael Flor,
Prof. Dr. rer. nat. Dr. h.c. Wolffried Stucky, Prof. Dr. rer. nat. Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

==============================================================================