- From: <herman.ter.horst@philips.com>
- Date: Thu, 6 Nov 2003 19:19:02 +0100
- To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org
>>[...] >> >>>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. The word finite has not been removed from the statement of the rdfs entailment lemma in the appendix. > >>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. It seems that this is change is not consistently applied to the document. The definition of rdfs interpretation includes "which contain only names form V union rdfV union rdfsV". This phrase should be removed, and similarly for rdf interpretations. > >> >>== >> >> >>>> >>>>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. ) I agree that the mapping sur is an improvement over the previous mapping '. There are however problems in the case of the rdfs entailment lemma. See my separate mail on the rdfs entailment lemma. [...] > >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 > > Herman
Received on Thursday, 6 November 2003 13:19:52 UTC