Re: no explicit type on bnodes

From: Jeremy Carroll <jjc@hpl.hp.com>
Subject: no explicit type on bnodes
Date: Fri, 20 Jun 2003 13:53:09 +0300

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

Both of these make the change much less desirable in my eyes.
Exceptions to ``all blank node typing is optional'' make it harder to
determine just what needs to be typed.  Changes to the semantics just to
support this change impose a significant cost.

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

What is the direct semantics of an RDF graph?  Do you mean that any
ontology whose translation is G has the same meaning as any ontology whose
translation is G plus the missing type triple?  This is a large part of
what needs to be shown.

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

Not correct.  The missing triples may be RDFS consequences of G plus a
graph that carries some of the OWL semantic conditions, but they certainly
are not 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

This is Theorem 2 from S&AS, but Theorem 1 also needs to be demonstrated.

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

If b is in the graph, then it is in some triple.

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

This introduces a form of non-monotonicity
 _:b <ex:ap> "1" .
 <ex:ap> rdf:type owl:AnnotationProperty .
would entail 
 _:b rdf:type owl:Thing .
but
 _:b <ex:ap> "1" .
 <ex:ap> rdf:type owl:AnnotationProperty .
 _:b rdf:type owl:Ontology .
would not.

> 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 don't see how this second half demonstrates 3).

>  ++++
> 
> I've j[us]t discovered this msg sitting on my desktop - I think it's finished, 
> if not I guess someone will point it out.

I'm not sure if you got around to 

> [...], and then have further discussion of facts 
> individual()

> Jeremy

peter

Received on Thursday, 24 July 2003 10:19:25 UTC