Re: RDF Semantics: RDFS entailment lemma

...

>>>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
>>>invoked.
>>
>>Why?
>
>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,
rdfs11.
It seems that the validity of this rule is not yet guaranteed by
a corresponding condition in the definition of rdfs interpretations.

Herman

>> Herman ter Horst

Received on Wednesday, 16 April 2003 12:17:05 UTC