Re: RDF Semantics: RDFS entailment lemma

At 21:40 13/04/2003 -0500, pat hayes wrote:

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

I don't think the modification to rdfs7a is needed, though I do agree the 
new rule is.  (I tried working with the simple fact [rdf:type rdfs:domain 
rdfs:Resource .] but then realized that's not strong enough.)

So given:

   rdf:type rdfs:subPropertyOf xxx .
   xxx rdfs:domain yyy .
->
   rdfs:Resource rdfs:subClassOf yyy .

and

[1]  type subproperty p .
[2]  p domain d .
[3]  a type b

->

[4]  Resource subClassOf d           ([1],[2],above)

      type range class                (table 3.3)
      b type class                    ([3], rdfs3)
[5]  b subclass resource             (rdfs7a)

      b subclass d                    ([5],[4],rdfs8)

...

It is also possible to show d is a subclass of resource:

      domain range class              (table 3.3)
      d type class                    ([2], rdfs3)
      d subclass resource             (rdfs7a)

...

I think your revised 7a can already be derived:

[6]  xxx type Class
[7]  Resource subClassOf yyy

->

[8]  xxx subClass Resource          ([6],rdfs7a)
      xxx subClassOf yyy             ([8],[7],rdfs8)


#g


-------------------
Graham Klyne
<GK@NineByNine.org>
PGP: 0FAA 69FF C083 000B A2E9  A131 01B9 1C7A DBCA CB5E

Received on Monday, 14 April 2003 08:26:59 UTC