# RDF Semantics: partial review

From: <herman.ter.horst@philips.com>
Date: Wed, 15 Oct 2003 18:11:58 +0200
To: pat hayes <phayes@ihmc.us>

Message-ID: <OF95F4750B.925210D2-ONC1256DC0.004C56AC-C1256DC0.005911B3@diamond.philips.com>
```
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.

==

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

==

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?

==

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))
<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 Wednesday, 15 October 2003 12:14:35 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 7 January 2015 14:54:08 UTC