RDF Semantics: a partial review

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