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. 

I agree that my two examples follow from the new rule rdfs12, and that
this rule is valid.
And I agree with Graham Klyne that the new rule rdfs7a follows
from the old rule rdfs7a, so can be replaced by it.

>But your example has some 
>other consequences: in fact, it entails that Resource is a subClass 
>of Class, ie that everything is a class.

How do you obtain this?

>
>In order to prove the closure lemma, I need to somehow show that this 
>is the *only* way that the above entailment rule could possibly be 
>invoked. 

Why?

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

I'm not sure whether these last two paragraphs are justified.
Couldn't you also say that the new rule rdfs12 shows that the
rdfs does not enable one to make the domain of rdf:type 
or any of its superproperties any smaller than it is 
(i.e., rdfs:Resource) by adding other domain statements?

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

Regards,
Herman

Received on Monday, 14 April 2003 11:51:07 UTC