- From: <herman.ter.horst@philips.com>
- Date: Wed, 23 Apr 2003 17:30:19 +0200
- To: pat hayes <phayes@ai.uwf.edu>
- 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'. I was wondering about the question of validity, and about whether it would be possible to stay within the current theoretical context and within the current way of describing closure, as this might keep things simpler. It seems that the reasoning you describe might be captured without 'real inference rules' and without 'genuine variables', purely within the context of current RDF semantic theory and closure rules, by proving something like the following: "Lemma A" If the merge of an RDF graph G and the RDF statement x type A rdfs-entails the RDF statement x type B, where x is a uri not appearing in G, then G rdfs-entails the RDF statement A subclassof B. A corollory of such a "lemma" would be that the following more genuine closure rule would be rigorously valid: If the rdfs closure of G merged with x type A contains x type B, then the following may be added to the rdfs closure of G: A subclassof B. This resembles the deduction theorem of classical first-order logic (Hilbert style reasoning, no natural deduction). This "closure rule" might be applied at any time, using any pair of classes A and B. However, it would indeed be a huge step in terms of complexity and sophistication. Described in this way, it is not yet clear why a similar rule would not be needed for subPropertyOf. > >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. It seems that both lines of attack would need subtle reasoning with subinterpretations. For example, suppose that one wants to prove "Lemma A" above. Then an arbitrary rdfs interpretation I of G should be proved to satisfy A subclassof B. I can be extended to satisfy x type A, and be extended again to get an rdfs interpretation J of G merged with x type A. Then J satisfies x type B. But how to conclude that its subinterpretation I satisfies x type B? > > >>(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. It seems that this is not yet done in the version of yesterday. > >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 > > Herman

Received on Wednesday, 23 April 2003 11:44:35 UTC