From: pat hayes <phayes@ai.uwf.edu>

Date: Sun, 13 Apr 2003 21:40:36 -0500

Message-Id: <p05111b04babf8cfbbbe3@[10.0.100.6]>

To: herman.ter.horst@philips.com

Cc: www-rdf-comments@w3.org

Date: Sun, 13 Apr 2003 21:40:36 -0500

Message-Id: <p05111b04babf8cfbbbe3@[10.0.100.6]>

To: herman.ter.horst@philips.com

Cc: www-rdf-comments@w3.org

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 spamReceived on Sunday, 13 April 2003 22:40:44 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:15:20 UTC
*