RE: Discussion of WebOnt test I4.6-005

[cc'ed to Peter, because this mail implicitly talks about a proposed change to the correspondence theorem, without the need of the comprehension principles.]

>-----Original Message-----
>From: public-owl-wg-request@w3.org [mailto:public-owl-wg-request@w3.org]
>On Behalf Of Mike Smith
>Sent: Monday, January 05, 2009 11:07 PM
>To: W3C OWL Working Group
>Subject: Discussion of WebOnt test I4.6-005
>
>
>I'm hoping to reach consensus about how to handle WebOnt test
>[I4.6-005].  I believe that the test is applicable to both RDF and DL
>semantics, but is misleading.
>
>In DL semantics, the definition of entailment applies only to ontology
>models, so the annotation is irrelevant.  The test reduces to
>entailment of a declaration.
>
>In RDF semantics, the definition of entailment considers the annotation.
>
>First, we need to choose to accept this test case despite it being
>misleading, or reject it for being misleading.
>
>Second, I think we need a test case to make the difference in
>entailment definitions clear.  Something like
>
>O1
>Declaration(Class(A))
>
>O2
>Declaration(Class(A))
>AnnotationAssertion( rdfs:comment A "Anything" )
>
>In DL Semantics, O1 entails O2, in RDF semantics it does not.

Confirmed. It generally doesn't work, if the RHS graph of a checked entailment contains stuff that is syntactically valid OWL 2 DL, but is not interpreted by the Direct Semantics. Other examples are the use of ontology properties (owl:incompatibleWith) or deprecations (C type DeprecatedClass).

Note that this is reflected in the current version of the OWL 2 Correspondence Theorem in the RDF-Based Semantics.

>Thoughts appreciated.

There is another important point to keep in mind for all tests for OWL 2 DL and OWL 2 Full. In OWL 2 Full, the so called "comprehension principles" are not part of the normative semantics anymore, hence certain OWL 2 DL entailments are not OWL 2 Full entailments anymore. 

However, this change to OWL 1 is not as dramatic as it might look. I am currently working on this stuff (proving the correspondence theorem, and intending to revising it), and found the following: Every OWL 2 DL entailment query can easily be syntactically "normalized" (I don't have a better word at the moment) in a way, that its semantics doesn't change wrt the Direct Semantics, and that if the entailment holds under the Direct Semantics, then it also holds in OWL 2 Full. 

So one can, from a semantic point of view, really still say that /every/ OWL 2 DL entailment is also a OWL 2 Full entailment. The only difference to OWL 1 is that there will be syntactic variants of an entailment, for which this relationship does not hold. But I don't regard this to be relevant for the correspondence, in particular because the "normalization" is straightforward, and will even be easy to spot by humans looking to an entailment query (see below for the approach). A very nice consequence is that the comprehension principles are redundant for this form of correspondence between DL and Full. (Perhaps not in general for Full, though, I still need to check this point in more detail, but it's not relevant for our discussion here).

Here is the idea:

1) Discover all the class expressions (booleans, enumerations, property restrictions) and datatype restrictions on the right-hand-side graph of the queried entailment. Note that for OWL 2 DL ontologies in RDF graph form (and nothing else is of interest for the correspondence between DL and Full) the reverse RDF mapping actually realizes such a thorough syntactic discovery process, so this is effectively doable by a computer program.

2a) For each such discovered class expression CE: Build a triple t_CE of the form "CE rdfs:subClassOf owl:Thing". Note that w.r.t. the Direct Semantics these triples are tautologies. (However, they are not tautologies w.r.t. the RDF semantics, because CE consists of existential assertions about individuals having certain specific class extensions.).
 
2b) For the datatype restrictions, it's a bit more complicated AFAICT. I suggest to put a universal property restriction on owl:bottomDataProperty and the datatype restriction, and for the constructed property restriction CE, which is a class, a subClassOf-Thing axiom t_CE is then build in the way described above. This is a tautology again. (FIXME: Is there a simpler way to treat datatype restrictions?)
 
3) Add all the triples t_CE to the left-hand-side graph of the queried entailment (it might be necessary to substitute bNodes).

Now, the adjusted left-hand-side graph is still a valid OWL 2 DL ontology in RDF graph form, because only syntactically valid OWL 2 DL statements have been added. Under the Direct Semantics, the semantics of the left-hand-side graph has not changed, because only tautologies have been added. Hence, the semantic meaning of the queried entailment has not changed at all, it has only been /syntactically/ changed. It is a OWL 2 DL entailment if and only if the original query has been a OWL 2 DL an entailment. But now, if the adjusted query is an entailment w.r.t. the OWL 2 Direct Semantics, then it is also an entailment w.r.t. OWL 2 Full (proof currently under construction, but it seems to turn out that the proof will be almost identical to a proof for the current version of the theorem, the one using comprehension principles; there is a reason for this, but that's offtopic here).
 
My suggestion for the test cases:

It would be ugly (though straightforward) to adjust all the positive DL/Full entailment test cases in the way described above, in order to make them entailments for both DL and Full. I rather prefer to adjust the correspondence theorem accordingly, and there can then be a pointer to the section in the RDF-Based Semantics on how to "normalize" the entailments. I can do this within a few days.

(@Peter: The current version of the Correspondence Theorem is nonsense (though at least trivial to prove ;-)): It states that if G1 DL-entails G2, then G1 (Full+Principles)-entails G2. However, Full+Principles has turned out to be inconsistent, so this does not make much sense. In addition, the theorem isn't really useful for implementers, it doesn't give useful hints on how to write a good (and sound) Full reasoner that also covers the DL entailments. So I would like to change the theorem along the lines discussed above. The comprehension principles would still be in the document, because the approach above only safely works for DL ontologies in RDF graph form.)
 
Cheers,
Michael

--
Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web  : 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
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus