Re: RDF Semantics: rdfs entailment lemma / terHorst-proof-review

(I resend the mail that I sent yesterday, since it
was probably not clear that in the example
I meant Class with C.  In addition, I make two
small additions, marked with (A).)

When I went again over the proof of the rdfs entailment
lemma, to double-check all the details, I noticed that
there still seems to be an error in the lemma.
Perhaps I didn't see this earlier because the location
of the new error is extremely close to another, more
conspicuous error that I noticed last week and that
was solved with a change to the treatment of literals [1].

The new error also involves literals.
It can be described in terms of a testcase,
and there is a clear solution to the problem.

Testcase:
graph G containing only the triples
  v p l
  p range Class
where l is a literal.
Triple T:
  b subClassOf l
where b is a blank node.

This gives a counterexample to the rdfs entailment lemma.
According to the semantics, G rdfs-entails T.
   (Proof: Let I be an arbitrary rdfs-interpretation that 
   satisfies G.  Then <I(v),I(l)> in IE(I(p))
   and <I(p),I(Class)> in IE(I(range)).  By the semantic 
   condition on range, we get I(l) in CEXT(I(Class))=IC.
   Since IEXT(I(subClassOf)) is reflexive on IC, it follows
   that <I(l),I(l)> in IEXT(I(subClassOf)).
   Therefore, I satisfies T.)
However, the rdfs entailment rules do not derive T from G.
   (ls derives        v p b    -blank node b allocated to l
    rdfs3 derives     b t Class
    rdfs10 derives    b subClassOf b
    Here it stops.)

Proposed solution:
add new RDFS entailment rule:
"rdfs14" if E contains
   uuu aaa _:nnn where _:nnn is allocated to lll by lg
then add:
   uuu aaa lll
In the construction of the RDFS closure, rule "rdfs14" 
should be freely applicable at all times.

This new rule would be a kind of counterpart to rule lg.
It would also solve the problem with the proof.
The problem with the proof is the following step, near
the end:
   given "D contains a triple sur(SH+A(s)) p sur(SH+A(o))"
   conclude "this is an instance of" the triple spo
   "under the instantiation mapping x ->sur(A(x))".
The problem with this conclusion is that if o is a literal
and if b is the blank node allocated to o by rule lg,
then  sur(SH(o)) is b instead of o.
So this is *not* an instance in this case.  Calling the
instantiation mapping M, it can only be concluded that
the triple
   M(s) p b 
is in D.  When rule "rdfs14" would be present, we have
   M(s) p o
in D, as desired.

I confirm that I consider the rdfs entailment lemma to be
proved when this change would be made.

(A) The validity of "rdfs14" is clear.  There is no need
to make such an addition for the rdf entailment lemma.

===

I am afraid that with the comment above I express the
need to re-open the LC2 topic 'terHorst-proof-review'.
I hope that this error could be corrected before the 
PR publication.  Fortunately, it could easily be 
handled with the indicated solution.

===

I should also mention that the change to the treatment of
literals that was introduced last week seems to have made 
the Skolemization lemma false.

Since plain literals now also count as vocabulary, and
since plain literals cannot be "freely interpreted",
the interpretation I' cannot be constructed in general
in the way indicated in the proof.

There is a straightforward solution to this problem, by
sharpening the definition of Skolemization, for example
in the following way:
A Skolemization of an RDF graph G is an instance of
G with respect to an 1-1 instance mapping that maps
each blank node in G to a URI reference that does not appear
in G.
(A) (I omitted the word ground before instance since 
this is implied by the rest of the definition.)

The Skolemization lemma plays only a peripheral role
in the RDF Semantics document, since it is not on the
path to the main completeness results.
Still, the lemma is relevant since, as the document notes
"Skolemization is routinely used in automatic inference
systems".


Herman ter Horst

[1] http://lists.w3.org/Archives/Public/www-rdf-comments/2003OctDec/0161.html

Received on Thursday, 20 November 2003 06:15:05 UTC