RE: completeness

Hi Peter!

You answered to Zhe:

>> And I think pD* vocabulary covers all the
>> core requirements Oracle sees on the field.
>
>I take this to mean that Oracle sees only the following constructs
>involving vocabulary from the owl: namespace
>
>- functional, inversefunctional, symmetric, transitive properties
>- object equality and inequality
>- inverse roles
>- equivalent classes and properties
>- existential, universal, and filler restrictions
>- disjoint classes
>
>This means no cardinalities at all, nor complements, nor deprecation,
>nor imports, nor ontology properties, nor use of owl:Thing or
>owl:Nothing.

* owl:Thing: I think this would only be an alias to rdfs:Resource, which is
in pD*, since pD* is an RDFS extention. So adding it wouldn't change the
semantics of pD* significantly. Analogue for owl:Class (aka rdfs:Class) and
owl:ObjectProperty (aka rdf:Property).

* owl:Nothing: I'm not certain whether an addition of owl:Nothing would be a
problematic step. My idea would be to simply add

  (11) I(owl:Nothing) in I(owl:Class)
  (12) ICEXT(I(owl:Nothing)) = EMPTYSET  

to the semantics of pD*. This would mirror the way how owl:Nothing is
handled in OWL-Full. This *would* actually lead to additional entailments
(below is an example), so this would require additional triple rules. But I
don't see at the moment where this would lead to problems.

* Ontology properties, esp. owl:import (together with owl:Ontology): Here I
don't see a real problem, too, at the moment. In OWL-Full, the distinctive
feature of ontology properties is that they have domains and ranges of
owl:Ontology. So this looks to me as if it would be largely sufficient to
just add a few additional "axiomatic triples" like e.g.

  owl:priorVersion rdfs:range owl:Ontology
    
I will need to think a bit further on this. In the end, ontology properties
are special to OWL, anyway, and need to be introduced for OWL specifically.
In comparison, there aren't ontology properties in sROIQ and the other
description logics, which build the foundation for OWL-DL and its proposed
fragments. So I would ask why should there be ontology properties in pD*?

>It also means no inferences *from* existential restrictions, and no
>inferences *of* universal restrictions.  Also no inferences *of*
>unmentioned existential restrictions or unmentioned filler 
>restrictions.
>
>Also very limited inference *of* subclass and subproperty 
>relationships,
>and equivalent classes and properties.  
>
>Similarly, limited inference
>*of* same individuals and no inference *of* distinct individuals.  Also
>no inference *of* property functionality, inverse functionality, or
>symmetricity, transitivity.
>
>To see the sort of thing that is lost in pD*, consider that
>
>p rdf:type C .
>q rdf:type D .
>C owl:disjointWith D .
>
>does not pD* entail 
>
>p owl:differentFrom q .

Yes, but I believe one can at least "simulate" this adequately: One can add
to the LHS of the queried entailment an additional 'sameAs' triple, which
leads to:

  (21) p rdf:type C
  (22) q rdf:type D
  (23) C owl:disjointWith D
  (24) p owl:sameAs q

and then check whether a contradiction is entailed:

  (40) p rdf:type owl:Nothing

For this to get, my suggestion (12) above for a semantics of owl:Nothing
would be sufficient, since it is possible to get from pD* semantics and
(21)-(24)

  (50) I(p) in EMPTYSET

which leads to (40) via RDFS semantics and (12).

To see (50): From (21),(22) and (24) one can conclude

  (60) p rdf:type D

This is true because, while in pD* the semantics of owl:sameAs is /not/ "=",
it is at least defined to

  * be an equivalence relation on I(rdfs:Resource), and

  * provide a "substitution principle" of the form:

     x p y
     x owl:sameAs x'
     y owl:sameAs y'
     ---------------
     x' p y'

Because owl:sameAs is an equivalence relation, it is reflexive and
symmetrical. So we can specialize the general substitution principle to our
purpose:

  q rdf:type D     # (22)
  q owl:sameAs p   # (24) + symmetry of owl:sameAs
  D owl:sameAs D   # reflexivity of owl:sameAs
  --------------
  p rdf:type D

which is (60).

So from (21) and (60) we receive by RDFS semantics:

  (70) I(p) in ICEXT(I(C)) ^ ICEXT(I(D))

And axiom (23) provides:

  (80) ICEXT(I(C)) ^ ICEXT(I(D)) = EMPTYSET

Taken together, from (70) and (80) we receive (50). 

>Nor does
>
>p r q .
>
>pD* entail
>
>p rdf:type _:e .
>_:e owl:hasValue q .
>_:e owl:onProperty r .

This entailment is actually explicitly supported by pD*. In this case even
the converse entailment exists (a rare case of "iff"-semantics in pD*). The
respective semantic condition is given by Definition 5.1 in [10]:

  If 
    (a, b) in E_I(I(hasValue)) 
    and (a, p) in E_I(I(onProperty)), 
  then 
      x in CE_I(a) 
    if and only if 
      (x, b) in E_I(p),

where "E_I(.)" denotes a property extention, and "CE_I(.)" denotes a class
extention.

Note that RDFS semantics allows me to get from

  x in CE_I(a)

to

  (x, a) in E_I(I(rdf:type))

So I really can perform the entailment check for the triples you mention
above.

>Nor does 
>
>p rdf:type _:s .
>_:s owl:someValuesFrom C .
>_:s owl:onProperty r .
>
>pD* entail
>
>p r _:x .

Not in pD*, but in "pD*sv", an extention to pD*, which is also specified in
the paper (Definition 6.1). 

However, AFAICS, for pD*sv the paper only provides a completeness result
w.r.t. triple rules. I did not find a complexity bound, neither for
entailment nor for consistency, in contrast to the bounds which exist for
pD*. So pD*sv might be a little too much as a foundation for OWL-Prime.

Of course, there are still a lot of "missing" entailments in pD*, and
several of them are listed in the pD* paper itself (sec. 1.8 provides a nice
list of examples).

Cheers,
Michael

[10] <http://linkinghub.elsevier.com/retrieve/pii/S1570826805000144>

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