RDF Semantics review: RDFS closure lemma / entailments from empty graph

RDF Semantics document,
last call version, 23 january 2003
This comment was mailed earlier to the WebOnt WG [1].


Consideration of rdfs-entailments from the empty RDF graph
shows that there is an error in the RDFS entailment lemma.
In line with the definition in 3.3, one triple
should be entailed for each of the 13 entries following
"IC contains":
  rdfs:Resource rdf:type rdfs:Class .
etc.
(including a triple
  rdfs:XMLLiteral rdf:type rdfs:Class .
although rdfs:XMLLiteral does not appear in the table in 3.3)
and one triple should be entailed for each of the
entries following "IP contains":
  rdf:type rdf:type rdfs:Property .
etc.
Each of these 13 + 16 + aleph-0 triples
(16 is counted without duplicates; the "aleph-0 triples" are 
from rdf:_1 etc.) follows by using the axiomatic triples in 
combination with the closure rules from 4.2, apart from one 
of these triples:
The triple
  rdf:value rdf:type rdfs:Property .  (*)
is rdfs-entailed by but is not in the rdfs-closure of the empty 
rdf graph, since rdf:value never appears in either the
axiomatic triples or the closure rules.

(This gives a test case for this problem:
according to the normative definition, the empty graph
rdfs-entails the triple (*), but this is not confirmed
by the rdfs entailment lemma.)

In particular, moreover, each of the 11 triples mentioned
under part 1. of the definition of rdfs closure
can safely be omitted from that definition.
(Note that one of these 11 triples,
  rdf:nil rdf:type rdf:list .
is already in the definition of rdf closure.)

The following 4 derivation patterns suffice for each
of these 13 + 15 + aleph-0 proofs
(This might be added to the proof sketch of the
rdfs entailment lemma):
I
  x rdfs:range y .
  rdfs:range rdfs:domain rdf:Property .
  rdfs:range rdfs range rdf:Class .
together imply
  x rdf:type rdf:Property
  y rdf:type rdf:Class
II
similarly for domain instead of range
III
  rdfs:subClassOf rdfs:domain rdfs:Class .
  rdfs:subClassOf rdfs:domain rdfs:Class .
  x rdfs:subClassOf y .
together emply
  x rdf:type rdfs:Class .
  y rdf:type rdfs:Class .
IV
similary for subPropertyOf instead of subClassOf 

(For the proofs involving rdf:_1 etc. also the triples from 
part 2. of the definition of rdfs closure are used.)

Herman ter Horst
Philips Research

[1] http://lists.w3.org/Archives/Public/www-webont-wg/2003Feb/0313.html

Received on Friday, 21 February 2003 11:27:26 UTC