From: <herman.ter.horst@philips.com>

Date: Thu, 24 Apr 2003 14:49:43 +0200

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF83C287FC.B40E0632-ONC1256D12.004076E6-C1256D12.00469DD6@diamond.philips.com>

Date: Thu, 24 Apr 2003 14:49:43 +0200

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF83C287FC.B40E0632-ONC1256D12.004076E6-C1256D12.00469DD6@diamond.philips.com>

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

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:15:20 UTC
*