Re: RDF Semantics: RDFS entailment lemma

In my email of yesterday [1] I described a lemma that might be of use
to realize the program sketched by Pat for proving the RDFS entailment
lemma, within the framework of the theory described in the RDF Semantics
document.  In particular, the lemma provides a closure rule generating
subclassof statements.  (It is not yet completely certain that the
current notion of rdfs closure generates enough subclassof statements
to make the RDFS entailment lemma true.)
Here is a more complete statement of the lemma and closure rule, together
with a proof:

Lemma A
Suppose that the rdf graph G rdfs-entails  A type class  and B type class,
and that the uri x does not appear in G or rdfsV or rdfV.
Suppose that G merged with  x type A  rdfs-entails  x type B.
Then G rdfs-entails  A subclassof B.

Proof.  (Contrary to what I said yesterday, this does not require
reasoning with subinterpretations.)  Let I be an rdfs-interpretation
of G.  Since G rdfs-entails  A type class  and B type class, it 
only needs to be proved that ICEXT(I(A)) subsetof ICEXT(I(B)).
Let z be in ICEXT(I(A)).
Change I slightly to become an interpretation I', the only change
being that I'(x)=z.  I' is also an rdfs-interpretation: only the
value I'(x) needs to be added (if x is not in the vocabulary of I)
or changed (if x is in the vocabulary of I but I(x) unequal z).
Since x does not appear in G, I' satisfies G and  x type A.
Hence I' satisfies x type B, so z=I'(x) is in ICEXT(I(B)).

Corollary.  The following closure rule for subclassof is valid:
Suppose the closure of G contains A type class and B type class,
and that the uri x does not appear in G or rdfsV or rdfV.
Suppose that the closure of (G merged with  x type A) contains
x type B.  Then the following may be added to the closure of G:
A subclassof B.

Similar results hold, with a similar proof, for subpropertyof:

Lemma B
Suppose that the rdf graph G rdfs-entails  p type property  and
q type property,  and that the uri's x and y do not appear in G 
or rdfsV or rdfV. 
Suppose that G merged with  x p y  rdfs-entails  x q y.
Then G rdfs-entails  p subpropertyof q.

Corollary.  The following closure rule for subpropertyof is valid:
Suppose the closure of G contains  p type property  and  q type property,
and that the uri's x and y do not appear in G or rdfsV or rdfV.
Suppose that the closure of (G merged with  x p y) contains
x q y.  Then the following may be added to the closure of G:
p subpropertyof q.


I cannot yet provide the next step in the program for the proof,
that the closure lemma holds when the closure generation process
is extended with these two closure rules.
More precisely, it is not clear whether the if-semantic conditions for
subclass of and subpropertyof hold for the Herbrand interpretation
of this extended rdfs closure of an rdf graph.

Comments?

Herman

[1] 
http://lists.w3.org/Archives/Public/www-rdf-comments/2003AprJun/0094.html


PS   In [1] I made a mistake:

>>>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.
>>
>>Indeed, an editorial slip. Thanks for catching this, I will fix it at 
>once.
>
HtH>It seems that this is not yet done in the version of yesterday.

I am sorry: it was already done.

Received on Thursday, 24 April 2003 08:51:26 UTC