- From: <herman.ter.horst@philips.com>
- Date: Fri, 17 Oct 2003 09:23:09 +0200
- To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org
Sorry - I sent this mail to rdfcore instead of rdfcomments. Resending it below, I make a few additions, marked by (A) and based on further reading in the document. Partial review of yesterday's version of the RDF Semantics document at http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.4.html Although I have not yet looked in detail at the RDFS entailment lemma proof, it seems safe to say that the new proof appendix is an improvement. (A) It is very nice that there is now such a short proof of the interpolation lemma, that the proofs of the rdf and rdfs entailment lemmas follow a more direct pattern than before, and that more details are provided for the rdf and rdfs entailment lemmas. == The current definition of simple entailment reads: >a set S of RDF graphs (simply) entails a graph E if every >interpretation [of the vocabulary of (S union E)] which >satisfies every member of S also satisfies E (and similarly for rdf and rdfs entailment). The part between [] is added in the LC2 version. Without the part between [], transitivity of entailment is trivial: if S entails H entails G, then S entails G. I assume that each type of entailment (simple, rdf, rdfs) is still intended to be transitive. This is not made explicit in the document, and there seem to be several complications in the proofs that result from the addition between [], and which are not noticed in the text. For example, there seems to be a gap in the proof of the interpolation lemma. >Suppose S simply entails E *>Herb(S) satisfies S, so Herb(S) satisfies E To conclude * in the LC2 version, it needs to be certain that the vocabulary of Herb(S) includes that of E. This can be proved, with a lemma like the following: Lemma. If H simply entails G, then Voc(G) subsetOf Voc(H). Simple entailment is transitive: if S entails H entails G, then S entails G. (Proof: The first statement clearly implies the second statement. In order to prove the second statement, suppose that H entails G and that spo is in G while one of s,p,o is in Voc(G)-Voc(H). Let I' be the Herbrand interpretation of H union {spo} augmented with an arbitrary interpretation of V(G)-(V(H) union {s,p,o}). Let I be I', the only change being that the pair <s,o> is dropped from IEI(I(p)). Then I interprets V(H) union V(G), satisfies H but does not satisfy G.) A similar issue comes up with the RDF (RDFS) entailment lemma, but here it is much more complicated because the equivalent to the interpretation I just discussed needs to be proved to be an rdf(s)-interpretation. A detailed proof, if one can be given, would need to consider many cases. Wouldn't it be much simpler to go back to the LC definition of entailment, i.e. without the addition between []? Moreover, in order to prevent complicated interactions with axiomatic triples and their vocabulary, at several points the proofs seem to become simpler when each rdf-interpretation is assumed to interpret all of rdfV (and similarly for rdfs-interpretations). (A) I should explain this further. When the RDF(S) closure of a graph G is constructed by first adding *all* RDF(S) axiomatic triples, and then by applying the entailment rules, then the analogue of the above lemma for RDF(S) entailment is immediately obtained from the RDF(S) Herbrand interpretations, assuming that the part between [] is omitted from the definition of entailment (the entailment rules do not introduce further vocabulary): Lemma. If H RDF(S) entails G, then Voc(G) subsetOf Voc(H) u rdfV ( u rdfsV ). RDF(S) entailment is transitive: statement similar to that above. (For rdfs-entailment, the assumption that the RDFS closure of G does not contain an XML clash should be included.) == Near the end of the proof of the RDF entailment lemma, it seems that a conclusion is not justified: Given a mapping A from blank(E) to IRRH such that RH+A satisfies every triple spo in E, it does not follow that <RH+A(s)',RH+A(o)'> is in IERH(p). It does follow that <RH+A(s),RH+A(o)> is in IERH(p). To conclude the proof, a function A':blank(E)->IRRH can be defined by A'(b)=b' if A(b)=xml(l) for some well-typed XML literal l, where the blank node b' is allocated to l, and by A'(b)=A(b) otherwise. Then, for each triple spo in E, I believe that by considering the possible cases for s and o (i.e., whether they are URI references, well-typed XML literals or other literals, or allocated or non-allocated blank nodes) it follows that <RH+A'(s)',RH+A'(o)'> is in IERH(p). This gives the desired subgraph of C that is an instance of E. == I do not see the reason to make use of the literal generalization rule. The proof of the rdf-entailment lemma uses rule lg only, in the construction of C, for triples with well-typed XML literals in object position, and for this case the same newly generated triple can also be obtained with rule rdf2, which would then generate two triples. Of course, the if side of the lemma doesn't need it either. Or am I overlooking something? (A) I now see that the RDFS entailment lemma uses lg in a way not subsumed by other rules. It seems that the RDF entailment lemma could omit the use of lg. == In the proof of the RDF entailment lemma, it would be appropriate to say explicitly what the domain and range of the mapping x |-> x' is: nodes(C) respectively IR. It seems that the last case of this definition ("if x is allocated to any other literal lll by rule lg then x' is lll itself") could be omitted, since lg (or rdf2, see previous remark) is only applied to triples with well-typed XML literals in object position. == In the definition of the RDF Herbrand interpretation RH, in the definition of IEXTRH(x), it seems that the 'otherwise' case can be omitted, as well as the text between brackets that follows this table, since the domain of IEXTRH is IPRH. In other words, there is no 'otherwise'. == It seems that in the definition of RH, the set IR needs to include only the URI references in node position. == The table in Section 4 with the RDFS semantic conditions seems to have an error: If x is in IC, then it should be <x,I(rdfs:Resource)> is in IEXT(I(rdfs:subClassOf)) instead of <x,IR> is in IEXT(I(rdfs:subClassOf)) == The proof of the interpolation lemma uses a subscript Herb(G) which should be Herb(S). == Proof of rdf entailment lemma: instead of "RDF subinterpretation", it should be RDF interpretation. Herman ter Horst
Received on Friday, 17 October 2003 03:25:01 UTC