RDF Semantics: RDFS entailment lemma

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.

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

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

Herman ter Horst

Received on Thursday, 10 April 2003 09:34:29 UTC