- From: pat hayes <phayes@ai.uwf.edu>
- Date: Wed, 16 Apr 2003 15:59:12 -0500
- To: herman.ter.horst@philips.com
- Cc: www-rdf-comments@w3.org

>... > >>>>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 . (*) It does not mean that, indeed. It is meant that a derivation exists of the following form: xxx type A .... xxx type B ie *with the variable xxx (or indeed any other expression) in place* throughout the derivation. If one can do that, then that entailment must hold for *every* xxx (under any other assumptions that are used in the derivation); and if that is true, then A subClass B must also be true (or, a consequence of those other assumptions). Your example provides just such a subproof with a variable: given that we assume rdf:type rdfs:subPropertyOf P . P rdfs:domain yyy . then we can derive as follows: xxx type A . xxx P A . xxx type yyy . But of course then one has to allow these inference rules to be treated not merely as closure rules, but more like real inference rules in a natural deduction logic where there are genuine variables in the language. I have no problems with this in principle; but we have gone to considerable lengths to try to keep the RDF semantics simple, and rules like this would be a huge step in terms of complexity and sophistication of the RDF 'proof theory'. There is a similar inference rule in natural deduction systems for classical logic, where the ability to derive Q from P is considered to be a proof of (P implies Q); in the above shorthand, ( P |- Q) |- (P implies Q). >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. Right, the proof needs to be modified. One way, sketched briefly in the document, is to talk about subinterpretations of Herbrand interpretations (which I may need to do in any case in order to handle the XMLLiterals properly). An alternative is to include the above inference rule in an extended rule set, prove the closure lemma with respect the the Herbrand interpretation of this extended notion of closure (which ought to be semi-obvious if it is stated properly), and the show that these 'extra' rules will produce the same extension as the existing rules, which will be tiresome but elementary. But this is only a plan of attack: I havnt tried writing this out yet. >(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. Indeed, an editorial slip. Thanks for catching this, I will fix it at once. Pat -- --------------------------------------------------------------------- IHMC (850)434 8903 or (650)494 3973 home 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32501 (850)291 0667 cell phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes s.pam@ai.uwf.edu for spam

Received on Wednesday, 16 April 2003 16:59:16 UTC