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