Re: RDF Semantics: RDFS entailment lemma

Herman, many thanks for your email and the careful checking you have 
done. Indeed I had not seen these inference paths. I am considering 
the possible options and will get back to you and the WG as soon as 
possible. Further comments below.

Brian, can you give this an ID (even though the last call is over, 
this is a bug that must be fixed.)

>It seems that the RDFS entailment lemma as currently stated
>in the RDF Semantics document (last call or editor's version)
>is not entirely correct.
>Consider the RDF graph G:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:domain y .
>This RDF graph rdfs-entails the triple
>   x rdfs:subClassOf y .
>( Proof: let I be an arbitrary rdfs interpretation of G.
>Clearly I(x) and I(y) are in IC.  Suppose z in ICEXT(I(x)),
>so <z,I(x)> in IEXT(I(rdf:type)).  The second triple shows
>that  <I(rdf:type),I(y)> in IEXT(I(rdfs:domain)).
>With the semantic condition on rdfs:domain it follows
>that z in ICEXT(I(y)), so that <I(x),I(y)> in
>IEXT(I(rdfs:subClassOf)). )
>However, this triple is not in the rdfs closure of G,
>unless x = y.

Most ingenious.

>(Proof: this closure contains the subClassOf statements
>   x rdfs:subClassOf x .
>   y rdfs:subClassOf y .
>but no other subClassOf statements involving x or y.)
>This example could be used as another closure rule ("rdfs11"),
>but then the RDFS entailment lemma would still be false.
>Namely, a slightly more complicated proof shows that
>the graph H:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:subPropertyOf p .
>   p rdfs:domain y .
>rdfs-entails the triple
>   x rdfs:subClassOf y .,
>but that this triple is not in the (extended definition of)

The most general form of the argument I can find is this:

type subProperty p .
p domain y .
x type z .


z subClass y .

which is a consequence of the '..and only if' condition on 
rdfs:subClassOf. The inference rule which naturally corresponds to 
this is rather more complicated than a closure rule: it is more like 
the implication-introduction rule in a natural deduction proof 
system, where one draws a conclusion from a entire subproof rather 
than a set of antecedents. It would look like this:

IF x rdf:type y . |- x rdf:type z .
THEN  y rdfs:subClassOf z .

where it is understood that x here must be a variable, ie in effect 
this antecedent amount so the proof that for all x, x type y implies 
x type z. This corresponds to the 'only if' part of the semantic 
condition on subClassOf.

Presumably there will be a similar phenomenon concerning 
subPropertyOf, which will require a similar extension to the rule 
base. I will try to cook up an example to illustrate this. As a first 
guess, I think it will start with

subProperty subProperty p .

>I found these examples in an attempt to become completely convinced
>of the truth of the rdfs entailment lemma.
>In this attempt I did become convinced of the "soundness" part of
>the lemma.

Right. That is pretty simple, of course. All the difficulty is in the 
completeness part.

>  For the "completeness" part of the lemma, it would perhaps
>be simpler, and still very useful, to restrict the lemma to
>"well-behaved" RDF graphs, which might be defined as RDF graphs which
>do not make (RDF) statements about built-in (rdf or rdfs) vocabulary
>in addition to the statements given by the axiomatic triples.

That is one possibility, although I am by no means sure that the 
fundamental problem is the 'bad-behaved' nature of your example: I 
think you have found a more basic weakness in the rule base, and that 
a 'well-behaved' graph could be constructed which would exhibit the 
same problem. And in any case I would prefer to have a more general 
solution if I can think of one in time :-)

I will get back to y'all in a few days when I get back from 
travelling and have time to digest this properly.


>Herman ter Horst

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	   for spam

Received on Thursday, 10 April 2003 11:57:35 UTC