W3C home > Mailing lists > Public > www-rdf-comments@w3.org > April to June 2003

Re: RDF Semantics: RDFS entailment lemma

From: <herman.ter.horst@philips.com>
Date: Wed, 16 Apr 2003 18:13:59 +0200
To: pat hayes <phayes@ai.uwf.edu>
Cc: www-rdf-comments@w3.org
Message-ID: <OF8ABACB8E.B40F0DF3-ONC1256D09.00537A17-C1256D0A.005951CA@diamond.philips.com>


>>>In order to prove the closure lemma, I need to somehow show that this
>>>is the *only* way that the above entailment rule could possibly be
>Because the entailment rule I mentioned
>(x type A |- x type B) |- A subClass B
>is in fact valid, and follows from the 'iff' in the semantic 
>condition on subClassOf. 

I would like to ask a further question and describe a simple example
that seems relevant.
What is the meaning of the antecedent of this rule,
(x type A |- x type B), described in more detail on the level of the 
closure generation process in Section 4.2?
It seems that the rule cannot mean the following:
apply the closure generation process with the current rules
rdfs1 - rdfs12; if, afterward, for each x type A, also x type B holds, 
then infer A subclass B.
For example, the RDF graph
  a type A .
  a type B .
  b type B .
does not rdfs-entail the RDF statement
  A subclass B . (*)
In terms of the proof in the appendix: the Herbrand interpretation
of the RDFS closure of this graph is not an RDFS interpretation because
the iff condition for subClassOf is not satisfied, in turn because
the statement (*) is not in the RDFS closure.
(For this reason this example seems to contradict the last-call version 
of the RDFS closure lemma, which does not yet introduce 
sub-rdfs-interpretations for dealing with XMLLiterals.)

>So in order to show that this rule can be 
>omitted from a complete rule base I have to show that any possible 
>application of it is already covered by some other inference path. 
>There is in fact a valid such rule for subPropertyOf as well, but no 
>way it could possibly be invoked by an RDFS subproof, so that one can 
>be safely omitted.
>>>The only way I can see how to do this at present is by an
>>>exhaustive analysis of the rule base, but I bet there is some elegant
>>>way to do it which I don't have time to think of.

Another comment related the rdfs entailment lemma: 
the latest editor's versions contain another new rdfs closure rule,
It seems that the validity of this rule is not yet guaranteed by
a corresponding condition in the definition of rdfs interpretations.


>> Herman ter Horst
Received on Wednesday, 16 April 2003 12:17:05 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:44:02 UTC