Re: RDF Semantics: a partial review

>[...]
>
>>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