no explicit type on bnodes

This is my final beer session action.

The idea is to change the mapping rules, so that for any rule which introduces 
a new blank node as its main node, then the explicit type triple in that rule 
is made optional. We will continue to refer to this triple as the explicit 
type triple (even though it is optional).

This is a little too ambitious, (it does not work), and I suggest retaining 
the restriction that unnamed ontologies must have an explicit type triple.

Moreover, I need a small tweak to the OWL Full semantics concerning the 
definition of the class extenstion of owl:DataRange.
Specifically any member of IDC that has a finite size is a member of the class 
extension of owl:DataRange.


Observations:

1) With the new mapping rules, the direct semantics of an RDF graph G missing 
one or more explicit type triples (for blank nodes) is the same as for the 
same graph augmented by the explicit type triples.

2) Under 1) the explicit type triples that must be added can be syntactically 
computed from G, except, that there may be any number of
_:b rdf:type owl:Thing .
corresponding to facts of the form
 individual()

3) All missing explicit type triples are RDFS consequences of G.

4) Given 2 and 3 then the correspondence theorem continues to hold, because 
given 2, and using the notation [G] to indicate the graph G with all missing 
explicit type triples added we have:

If G OWL-DL entails H
then
G RDFS entails [G] OWL-DL entails [H]
G RDFS entails [G] OWL-full entails [H}
G OWL-Full entails [H]
G OWL-Full entails H

The inverse is not true, but then that seems to be the case anyway. The 
inverse is only not true because:
a) [G] owl-DL entails [H]
does not follow from
[G] owl-full entails [H]

b) _:b rdf:type owl:Thing . is always true in OWL Full
but
individual() is not always true in OWL DL

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

I prove 2 and 3, and then have further discussion of facts 
individual()

=====
2) given a bnode b, from the mapping rules, then either there are no triples 
involving b, or one of the following is true.

a)
b rdf:type owl:Ontology .  is in G (*not* optional)

and this is the explicit type triple.

b)
b rdf:type blank . is in G

and explicit type is present or owl:Thing. 

c)
b rdf:type classID .  
classID rdf:type owl:Class . (or classID is a builtin class)
   are in G

and explicit type is present or owl:Thing. 

d)
b apID any .
apID rdf:type owl:AnnotationProperty . (or apID is a builtin annotation 
property)
   are in G
and
b rdf:type owl:Ontology .
  is not in G

and explicit type is present or owl:Thing. 

e)
b owl:unionOf any . 
   is in G

and explicit type is owl:Class

f)
b owl:intersectionOf any .
   is in G

and explicit type is owl:Class


g)

b owl:complementOf any .
   is in G

and explicit type is owl:Class

h)

b owl:oneOf any .
   is in G
and
 exists dpID such that
 dpID rdf:type owl:DatatypeProperty . 
   is in G
   (or dpID is a builtin datatypeproperty)
 such that
 either
  h.1)
   dpID range b .
    is in G
 or
 h.2)
  there is another blank node c with 
  c owl:onProperty dpID 
   in G
  and either
          c owl:allValuesFrom b .
        or
          c owl:someValuesFrom b .
  in G

and explicit type is owl:DataRange

i)

  b owl:oneOf any .
     is in G
  and
    h) does not apply

 and explicit type is owl:Class

j)
 b owl:onProperty any .
  is in G

and explicit type is owl:Restriction 

k)
  b rdf:first any .
  is in G

and explicit type is rdf:List .


That is an exhaustive analysis of the mapping rules, except
for the new rule (in red in the current editors draft) which
maps
individual() to
b rdf:type owl:Thing .

If this is a top-level fact then this may result in no triple
in the graph, since the explicit type triple is optional.

Otherwise we have either:

l)
any apID b .
apID rdf:type owl:AnnotationProperty .
  (or apID is a builtin annotationproperty)
 are in G

and explicit type of b is owl:Thing

or

m)
any opID b .
opID rdf:type owl:ObjectProperty .
  (or opID is a builtin individual valued property)
 are in G

and explicit type of b is owl:Thing .

Since the options a) through m) are mututally exclusive except for those that 
result in explicit type of owl:Thing; and moreover options a) through m) are 
an exhaustive analysis of the mapping rules, we have that any missing 
explicit type triple of blank nodes (other than owl:Ontology) can be deduced 
by syntactic analyis of G, or they are triples of the form
b rdf:type owl:Thing . 
  where b does not occur elsewhere in G.


3) analysing the cases above we see:

the empty ontology OWL Full entails

b rdf:type owl:Thing

(owl:Thing rdf:type owl:Class and
 owl:Class rdfs:subClassOf rdfs:Resource
and
 rdfs:Resource owl:equivalentClass owl:Thing
are all trivial)

The cases

e)
b owl:unionOf any . 
f)
b owl:intersectionOf any .
g)
b owl:complementOf any .
i)
  b owl:oneOf any .
     is in G
  and
    h) does not apply

 and explicit type is owl:Class

j)
 b owl:onProperty any .
k)

all follow by considering the rdfs:domain of the predicate of the given 
triple.

Case

a)
b rdf:type owl:Ontology . 

is trivial, since the explicit type triple is not optional.

Cases

b)
b rdf:type blank . is in G
c)
b rdf:type classID .  
d)
b apID any .
l)
any apID b .
m)
any opID b .

all have explicit type owl:Thing, which is trivially OWL Full entailed for any 
node.

Which leaves only case h).

[[
b owl:oneOf any .
   is in G
and
 exists dpID such that
 dpID rdf:type owl:DatatypeProperty . 
   is in G
   (or dpID is a builtin datatypeproperty)
 such that
 either
  h.1)
   dpID range b .
    is in G
 or
 h.2)
  there is another blank node c with 
  c owl:onProperty dpID 
   in G
  and either
          c owl:allValuesFrom b .
        or
          c owl:someValuesFrom b .
  in G

and explicit type is owl:DataRange
]]

This case follows because by the syntax of G the triple
b owl:oneOf any .
has object which is a (possibly empty) well-formed list of data literals, and 
from OWL Full semantics we have
if there exisits:
l, a sequence of x1,…,xn over LVI
then there exisits
y in IDC, <y,l> in EXTI(SI(owl:oneOf))

since this is finite, then y is also in the class extention of owl:DataRange, 
by the proposed tweak to OWL Full semantics.

Finished.


 ++++

I've jsut discovered this msg sitting on my desktop - I think it's finished, 
if not I guess someone will point it out.

Jeremy

Received on Friday, 20 June 2003 07:53:17 UTC