- From: pat hayes <phayes@ai.uwf.edu>
- Date: Thu, 10 Apr 2003 11:57:31 -0400
- To: herman.ter.horst@philips.com, Brian_McBride <bwm@hplb.hpl.hp.com>
- Cc: www-rdf-comments@w3.org

Herman, many thanks for your email and the careful checking you have done. Indeed I had not seen these inference paths. I am considering the possible options and will get back to you and the WG as soon as possible. Further comments below. Brian, can you give this an ID (even though the last call is over, this is a bug that must be fixed.) 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. Most ingenious. > >(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. The most general form of the argument I can find is this: type subProperty p . p domain y . x type z . rdfs-entails z subClass y . which is a consequence of the '..and only if' condition on rdfs:subClassOf. The inference rule which naturally corresponds to this is rather more complicated than a closure rule: it is more like the implication-introduction rule in a natural deduction proof system, where one draws a conclusion from a entire subproof rather than a set of antecedents. It would look like this: IF x rdf:type y . |- x rdf:type z . THEN y rdfs:subClassOf z . where it is understood that x here must be a variable, ie in effect this antecedent amount so the proof that for all x, x type y implies x type z. This corresponds to the 'only if' part of the semantic condition on subClassOf. Presumably there will be a similar phenomenon concerning subPropertyOf, which will require a similar extension to the rule base. I will try to cook up an example to illustrate this. As a first guess, I think it will start with subProperty subProperty p . .... >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. Right. That is pretty simple, of course. All the difficulty is in the completeness part. > 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. That is one possibility, although I am by no means sure that the fundamental problem is the 'bad-behaved' nature of your example: I think you have found a more basic weakness in the rule base, and that a 'well-behaved' graph could be constructed which would exhibit the same problem. And in any case I would prefer to have a more general solution if I can think of one in time :-) I will get back to y'all in a few days when I get back from travelling and have time to digest this properly. Pat > >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 Thursday, 10 April 2003 11:57:35 UTC