- From: pat hayes <phayes@ihmc.us>
- Date: Mon, 27 Oct 2003 14:54:17 -0500
- To: herman.ter.horst@philips.com
- Cc: w3c-rdfcore-wg@w3.org, "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

>[...] > >>So I will make the following changes: >> >>remove the vocabulary condition on entailment, as you suggest, ie the >>[ ] words (in four places); >> >>add the word 'finite' to the statements of the entailment lemmas, so >>that they read: "...iff there is a finite graph which can be >>derived...." See below. > > >>in the proofs, remove the words [which contain vocabulary from >>(vocab(S) union vocab(E) union crdfV)] from the definition of rdf(s) >>-closure., and the bracketted comment about vocabularies. >> >>and add the following to the end of the proof: >> >>'....so a subgraph of C is an instance of E, so C simply entails E. By >the >>compactness lemma, there is a finite subgraph of C which simply >>entails E and therefore satisfies the conditions of the lemma. QED " >> >>and similarly for the rdfs lemma (the wording is more delicate there). > >I believe that the rdf and rdfs entailment lemmas need an >additional assumption: it seems that E should be assumed to be >finite. True. I think that the best way to handle this is to just remove the word 'finite' from the statement of the lemmas, and add a remark in the appendix pointing out that if E is finite then the intermediate derived graph can also be taken to be finite. This restores the statements of the lemmas to their previous form without cluttering up the proofs. I will make this change. >Otherwise, the compactness lemma cannot be used in the way >you describe. > > >=== > >>>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). > > >[...] > >> >>Am I missing something? > >I should correct myself. It is not only that the proofs seem to >become simpler. >With the current (editorial version) formulation, >there seems to be an error in the rdf(s) entailment lemmas. > >As a example (testcase), consider the RDF graph G consisting just >of the triple > type type Property >Note that the Herbrand interpretation of G is an rdf-interpretation, >when an rdf-interpretation does not need to interpret all of rdfV. >Hence G, or the empty graph N, does not rdf-entail the RDF axiomatic >triple t: > subject type Property >However, the rdf-entailment lemma says that G or N do rdf-entail t, >since t can be derived, by means of zero rule applications, >from G or N combined with the RDF axiomatic triples. > >In view of this, it seems better to assume that each >rdf(s)-interpretation satisfies all of rdfV (and >therefore satisfies all RDF axiomatic triples). Yes, of course (now you have pointed it out :-). I will make this change. Peter has previously expressed a dislike for the 'crdV' construction, which was introduced only to keep the closures finite in any case and is therefore now irrelevant. > >== > > >>> >>>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. >> >>That is the mapping I intended to convey. Perhaps the prime notation >>is ambiguous. Suppose it read: >> >>.... [RH+A] satisfies every triple >>s p o . >>in E, i.e. IEXTRH(p) contains <([RH+A](s))',([RH+A](o))'> .... >> >>would that be clearer? I have made this change, anyway. > >I had interpreted RH+A(s)' exactly as you describe here, >([RH+A](s))'. However, this is another mapping than the one >I describe above. Indeed. After some soul-searching, subsequent to our conversation, I have reformulated this in terms of a mapping from XML values to surrogate nodes rather than the reverse. This makes the conclusion easier to state and more uniform with the RDFS case. (It establishes a slightly weaker result than the earlier argument form does, but nobody except you and I seems to care and I am too tired to write out the rather elaborate argument needed to cover the case where surrogates are used in the subject position but literals in the object position. ) >It seems to be helpful to mention that lg is not really needed in the >rdf entailment lemma. >Otherwise, a reader who discovers this is likely to be confused, as I >was. I have added the comment in the text of the proof, just after defining the closure: "Note also that the proof only requires that rule lg is used on well-typed XML literals, so that it actually establishes a slightly tighter result." >For example, Section 7 contains the following sentence (my emphasis): >>Subsequent rule sets for detecting RDF and RDFS entailment *need to >>be* supplemented with a special case of rule se1 which applies only >>to literals: literal generalization rule > I have replaced this with the non-modal wording: "Subsequent rule sets for detecting RDF and RDFS entailment use a special case of rule se1 which applies only to literals:" The revisions can be seen at http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.5.html Pat -- --------------------------------------------------------------------- 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@ihmc.us http://www.ihmc.us/users/phayes

Received on Monday, 27 October 2003 14:54:19 UTC