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>

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 >>>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 HorstReceived on Wednesday, 16 April 2003 12:17:05 UTC

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