From: <herman.ter.horst@philips.com>

Date: Wed, 19 Nov 2003 16:52:56 +0100

To: pat hayes <phayes@ihmc.us>

Cc: Brian_McBride <bwm@hplb.hpl.hp.com>, Dan Connolly <connolly@w3.org>, www-rdf-comments@w3.org

Message-ID: <OFFC277605.C7E47A54-ONC1256DE3.0029845C-C1256DE3.00574E22@diamond.philips.com>

Date: Wed, 19 Nov 2003 16:52:56 +0100

To: pat hayes <phayes@ihmc.us>

Cc: Brian_McBride <bwm@hplb.hpl.hp.com>, Dan Connolly <connolly@w3.org>, www-rdf-comments@w3.org

Message-ID: <OFFC277605.C7E47A54-ONC1256DE3.0029845C-C1256DE3.00574E22@diamond.philips.com>

When I went again over the proof of the rdfs entailment lemma, to double-check all the details, I noticed that there still seems to be an error in the lemma. Perhaps I didn't see this earlier because the location of the new error is extremely close to another, more conspicuous error that I noticed last week and that was solved with a change to the treatment of literals [1]. The new error also involves literals. It can be described in terms of a testcase, and there is a clear solution to the problem. Testcase: graph G containing only the triples v p l p range C where l is a literal. Triple T: b subClassOf l where b is a blank node. This gives a counterexample to the rdfs entailment lemma. According to the semantics, G rdfs-entails T. (Proof: Let I be an arbitrary rdfs-interpretation that satisfies G. Then <I(v),I(l)> in IE(I(p)) and <I(p),I(C)> in IE(I(range)). By the semantic condition on range, we get I(l) in CEXT(I(C))=IC. Since IEXT(I(subClassOf)) is reflexive on IC, it follows that <I(l),I(l)> in IEXT(I(subClassOf)). Therefore, I satisfies T.) However, the rdfs entailment rules do not derive T from G. (ls derives v p b -blank node b allocated to l rdfs3 derives b t C rdfs10 derives b subClassOf b Here it stops.) Proposed solution: add new RDFS entailment rule: "rdfs14" if E contains uuu aaa _:nnn where _:nnn is allocated to lll by lg then add: uuu aaa lll In the construction of the RDFS closure, rule "rdfs14" should be freely applicable at all times. This new rule would be a kind of counterpart to rule lg. It would also solve the problem with the proof. The problem with the proof is the following step, near the end: given "D contains a triple sur(SH+A(s)) p sur(SH+A(o))" conclude "this is an instance of" the triple spo "under the instantiation mapping x ->sur(A(x))". The problem with this conclusion is that if o is a literal and if b is the blank node allocated to o by rule lg, then sur(SH(o)) is b instead of o. So this is *not* an instance in this case. Calling the instantiation mapping M, it can only be concluded that the triple M(s) p b is in D. When rule "rdfs14" would be present, we have M(s) p o in D, as desired. I confirm that I consider the rdfs entailment lemma to be proved when this change would be made. === I am afraid that with the comment above I express the need to re-open the LC2 topic 'terHorst-proof-review'. I hope that this error could be corrected before the PR publication. Fortunately, it could easily be handled with the indicated solution. === I should also mention that the change to the treatment of literals that was introduced last week seems to have made the Skolemization lemma false. Since plain literals now also count as vocabulary, and since plain literals cannot be "freely interpreted", the interpretation I' cannot be constructed in general in the way indicated in the proof. There is a straightforward solution to this problem, by sharpening the definition of Skolemization, for example in the following way: A Skolemization of an RDF graph G is a ground instance of G with respect to an 1-1 instance mapping that maps each blank node in G to a URI reference that does not appear in G. The Skolemization lemma plays only a peripheral role in the RDF Semantics document, since it is not on the path to the main completeness results. Still, the lemma is relevant since, as the document notes "Skolemization is routinely used in automatic inference systems". Herman ter Horst [1] http://lists.w3.org/Archives/Public/www-rdf-comments/2003OctDec/0161.htmlReceived on Wednesday, 19 November 2003 10:53:42 UTC

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