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...."
>
>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.
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).


==


>>
>>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.
Given a mapping A from blank(E) to IRRH such that
RH+A satisfies every triple spo in E, it does
only follow directly that <RH+A(s),RH+A(o)> is in IERH(p)
for each spo in E.
 
>>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?
>
>No, you are correct. The only cases of rule lg that are needed in the 
>RDF proof are those which support the rule rdf2. I have phrased the 
>rules this way as it seemed more elegant to have rules with a single 
>conclusion; and the RDFS case requires all literal generalizations to 
>be done, as even ill-typed literals must be mappable into subject 
>position in order to exposed.
>
>>(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.
>>

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



Herman

Received on Tuesday, 21 October 2003 07:53:34 UTC