Re: RDF Semantics: RDFS entailment lemma

Herman, greetings. Your example (below) has sparked quite a lot of 
work. I think I now understand what is going on in it and how to 
handle it, so this is an attempt to summarize and explain.

The key pattern is the following combination:

type subproperty p .
p domain d .

Together, these support an inference path from any type assertion to 
another type assertion:

a type b
a p b        (using rdfs6)
a type d   (using rdfs2)

and hence, since a could be anything,  support an entailment

b subClass d

which however is not inferrable at present.  The 'natural' 
corresponding inference rule would be the one I mentioned:

if [a type b .] entails [a type c .], then infer  [b subclass c .]

which is not a closure rule. Including this rule would be 
semantically elegant but computationally ugly, so Ive been trying to 
find a way to avoid it.

(BTW, I now think I was wrong to worry that there was a corresponding 
case for subPropertyOf, as the inference path for the corresponding 
antecedent subproof would have to go from a P b to a Q b for any a 
and b, and I cannot see any such pathway which does not already 
involve an assertion of subPropertyOf, since there is no property 
corresponding to binary predication in the way that rdf:type does to 
unary predication.)

The entailment you noted actually follows from a further observation, viz that

a type Resource

is always true for any a; so using the above reasoning gives

Resource subClass d

as an entailment of the two initial triples alone, with no further 
assumptions. And is in fact follows by the kind of semantic analysis 
that you performed, more directly.  Now, this in turn can only be 
interpreted as saying that the class extension of d is the same as 
rdfs:Resource, an equation I had not previously thought possible to 
express in RDF (and which means I have to rewrite rule rdfs7, see 
below)

However, this (unexpectedly strong) conclusion does mean, I think, 
that this entire phenomenon can be captured by a single special rule, 
viz:

rdf:type rdfs:subPropertyOf xxx .
xxx rdfs:domain yyy .
entails
rdfs:Resource rdfs:subClassOf yyy .

and a modification to rdfs7a, viz:

xxx rdf:type rdfs:Class .
rdfs:Resource rdfs:subClassOf yyy .
entails
xxx rdfs:subClassOf yyy .

(which covers the previous version since
rdfs:Resource rdfs:subClassOf rdfs:Resource .
follows trivially by rdfs 7b)

The conclusion in your example then follows directly, since of course 
all classes are subclasses of Resource. But your example has some 
other consequences: in fact, it entails that Resource is a subClass 
of Class, ie that everything is a class.

In order to prove the closure lemma, I need to somehow show that this 
is the *only* way that the abovve entailment rule could possibly be 
invoked. The only way I can see how to do this at present is by an 
exhaustive analysis of the rule base, but I bet there is some elegant 
way to do it which I don't have time to think of.

The general pragmatic conclusion seems to be that it is definitely 
not a good idea to try to say  things about superproperties of 
rdf:type, for sure :-) I propose to add the following paragraph as a 
'warning' and also a brief commentary on this new rule:

--------
The rule rdfs11 is a technicality, required in order to ensure the 
truth of the following lemma. It is unlikely to be used in practice, 
and will normally only produce redundant inference paths for some 
items in the closure. In general, the property rdf:type is best 
considered to be part of the logical machinery; as this rule 
illustrates, imposing gratuitous conditions on rdf:type can produce 
unexpected entailments. Similar strange conclusions can arise from 
asserting that rdfs:Resource is a subclass of another class, for 
example, or asserting unintuitive properties of rdfs:Class.
--------

Any comments?

Pat

>It seems that the RDFS entailment lemma as currently stated
>in the RDF Semantics document (last call or editor's version)
>is not entirely correct.
>
>Consider the RDF graph G:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:domain y .
>
>This RDF graph rdfs-entails the triple
>   x rdfs:subClassOf y .
>
>( Proof: let I be an arbitrary rdfs interpretation of G.
>Clearly I(x) and I(y) are in IC.  Suppose z in ICEXT(I(x)),
>so <z,I(x)> in IEXT(I(rdf:type)).  The second triple shows
>that  <I(rdf:type),I(y)> in IEXT(I(rdfs:domain)).
>With the semantic condition on rdfs:domain it follows
>that z in ICEXT(I(y)), so that <I(x),I(y)> in
>IEXT(I(rdfs:subClassOf)). )
>
>However, this triple is not in the rdfs closure of G,
>unless x = y.
>
>(Proof: this closure contains the subClassOf statements
>   x rdfs:subClassOf x .
>   y rdfs:subClassOf y .
>but no other subClassOf statements involving x or y.)
>
>This example could be used as another closure rule ("rdfs11"),
>but then the RDFS entailment lemma would still be false.
>Namely, a slightly more complicated proof shows that
>the graph H:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:subPropertyOf p .
>   p rdfs:domain y .
>rdfs-entails the triple
>   x rdfs:subClassOf y .,
>but that this triple is not in the (extended definition of)
>closure.
>
>I found these examples in an attempt to become completely convinced
>of the truth of the rdfs entailment lemma.
>In this attempt I did become convinced of the "soundness" part of
>the lemma.  For the "completeness" part of the lemma, it would perhaps
>be simpler, and still very useful, to restrict the lemma to
>"well-behaved" RDF graphs, which might be defined as RDF graphs which
>do not make (RDF) statements about built-in (rdf or rdfs) vocabulary
>in addition to the statements given by the axiomatic triples.
>
>Herman ter Horst


-- 
---------------------------------------------------------------------
IHMC					(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola              			(850)202 4440   fax
FL 32501           				(850)291 0667    cell
phayes@ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam@ai.uwf.edu   for spam

Received on Sunday, 13 April 2003 22:40:44 UTC