From: pat hayes <phayes@ihmc.us>

Date: Mon, 29 Sep 2003 12:17:07 -0500

Message-Id: <p06001f37bb9e001c903e@[10.0.100.25]>

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-rdf-comments@w3.org

Date: Mon, 29 Sep 2003 12:17:07 -0500

Message-Id: <p06001f37bb9e001c903e@[10.0.100.25]>

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-rdf-comments@w3.org

> Comments on RDF Semantics (version dated 26 September 2003) > > >I did a quick read of the most of RDF Semantics, along with a careful >investigation of a couple pieces. Thanks. > Here are my comments. > >1/ The major new issue I have with the document is the unsupported change >of the entailment rules from informative to normative. Just for the record, that change happened a few versions ago; but your comment is noted. > >2/ The removal of the translation to LBase is a major improvement. I would >have prefered different wording in Section 0.1 concerning this translation >but can live with the new situation. > >3/ The document is of several minds with respect to just what the semantics >of RDF (and RDFS) is. There is wording in Section 1.3 to the effect that >the definition of the semantics of RDF and RDFS excludes the entailment >rules. How can this coexist with having the entailment rules be normative? Well, the rules are not part of the semantics as such. The issue of their normativeness (normativity? normitude?) seems to be orthogonal to this point. The Abstract of the document begins "This is a specification of a precise semantics, and corresponding complete systems of inference rules, for...." clearly indicating that the semantics is one thing, and the rules another, a division reflected in the organization of the document. (??Maybe I havnt followed your point here??) > >4/ The figures in the copy of the document that I reviewed have naming >problems, but I am told that these have since been fixed. They may not have been fixed to your satisfaction. The changes were largely graphical (color, font rendering) rather than textual. We have discussed the issue of the wording in figure 1, and I responded in an earlier message. > >5/ The Monotonicity and Compactness Lemmas are only stated for simple >entailment. However, readers could easily be left with the impression that >the other forms of entailment could also have the desirable properties that >accrue from these lemmas. The text states explicitly: "These results apply only to simple entailment, not to the extended notions of entailment introduced in later sections." reiterated after the statement of the anonymity lemma: "Note again that this applies only to simple entailment, not to the vocabulary entailment relationships defined in rest of the document.". Later, when RDF-entailment is introduced (section 3.1, second paragraph) the document repeats the warning, with a back-link and an illustrative example.: "It is easy to see that the lemmas in <a href>Section 2</a> do not all apply to rdf-entailment: for example..." I think this constitutes an adequate safeguard against this misunderstanding. > >6/ The characterization of simple entailment rules is misleading as they do >not currently correspond to the instance lemma. The comment on how to make >this change at the end of Section 7.1 does not adequately serve to correct >the misimpression. Let me suggest a re-wording and expansion of the first line of section 7.1 as follows. Would this be more acceptable? "The interpolation lemma in section 2 characterizes simple entailment in terms of instances and subgraphs. Being a subgraph requires no explicit formulation as an inference rule on triples, but one can give rules which generate generalizations, for example: " >7/ The document needs a better description of consistency and >inconsistency. Can you elaborate? Ah, I see that there is no glossary entry for 'consistent'; I will rectify this. > >8/ The change to the RDFS entailment lemma is incorrectly noted in the >change log as editorial. It was considered editorial because it was considered to be a correction of an error in the text rather than a change to the lemma. >9/ I view the development and statement of the entailment lemmas as >fundamentally flawed. I look for soundness and completeness in any such >syntactic characterization of entailment. Neither simple entailment, RDF >entailment, nor RDFS entailment have both these characteristics. In the sense of 'complete' you probably mean, that is correct. They never have been written in that style and I see no useful purpose to be served by so doing. >9a/ Section 7.1 does not provide any statement at all on whether the simple >entailment rules are complete with respect to simple entailment. Section 2 has already noted, however : "The interpolation lemma completely characterizes simple RDF entailment in syntactic terms. To tell whether a set of RDF graphs entails another, check that there is some instance of the entailed graph which is a subset of the merge of the original set of graphs. Of course, there is no need to actually construct the merge. If working backwards from the consequent E, an efficient technique ..." followed by a paragraph of discussion. The amended text (above) at the beginning of section 7.1 will refer back to this. I also note that section 7 begins by saying : "The following tables list some inference patterns which capture some of the various forms of vocabulary entailment." and does not refer to simple entailment. As you may recall, the inference rules in section 7.1 were introduced in order to ensure that the RDF and RDFS closures included appropriate generalizations of some of the entailed triples. >There is >a statement that the rules are sound, and that an agumentation of them >correspond to the instance lemma, but no proof is presented. That is true; however, I do not think that a proof is needed, as the relevant syntactic condition is fully described by the interpolation lemma. To provide a complete set of rules which implement the relevant search as a forward application of valid entailment rules would be computationally ridiculous. Since the main purpose of describing entailment rules in this document is not as an exercise in textbook formal logic, but rather to provide a useful guide to suggest relatively easy implementation styles for inference engines, to adopt the style you are here suggesting in the main body of the document would in my view serve no useful purpose and would likely be counterproductive. However, I plan to insert the following in the proof appendix (just after the QED of the interpolation lemma) , with a forward link from section 7.1 (end), which may go some way towards satisfying your point. (This change has not yet been discussed by the WG. ) --------- This lemma can be used as the basis for several different mechanical processes for checking simple entailment. One way to characterize entailment syntactically is in terms of inference rules which apply to a set S and can be used to derive E just when S entails E. For example, a slight modification of the simple entailment rules described in section 7.1 will suffice, where we allow new blank nodes to be allocated to existing blank nodes as well as to URI references and literals: extended simple entailment rules. ---------<table>------ Rule name If E contains then add xse1 uuu aaa xxx . uuu aaa _:nnn . where _:nnn is a blank node identifier allocated to xxx by rule xse1 or xse2. xse2 uuu aaa xxx . _:nnn aaa xxx . where _:nnn is a blank node identifier allocated to uuu by rule xse1 or xse2. ----------</table>-------- These rules allow blank nodes to proliferate, producing highly non-lean graphs; they sanction entailments such as ex:a exp ex:b . ex:a ex:p _:x . by xse1 with _:x allocated to ex:b ex:a ex:p _:y . by xse1 with _:y allocated to _:x _:z ex:p _:y . by xse2 with _:z allocated to ex:a _:u ex:p _:y . by xse2 with _:u allocated to _:z _:u ex:p _:v . by xse1 with _:v allocated to _:y It is easy to see that if S is an instance of T then one can derive T from S by applying these rules in a suitable sequence; the rule applications required can be discovered by examination of the instance mapping. So, by the interpolation lemma, S entails E iff one can derive (a graph containing) E from S by the application of these rules. However, it is also clear that applying these rules naively would not result in an efficient search process, since the rules will not terminate and can produce arbitrarily many redundant derivations of equivalent triples. The general problem of determining simple entailment between arbitrary RDF graphs is decideable but NP-complete. This can be shown by encoding the problem of detecting a subgraph of an arbitrary directed graph as an RDF entailment, using blank nodes to represent the graph (observation due to Jeremy Carroll.) ----------- > >SUGGESTION: I suggest that Section 7.1 be augmented with the following >Lemma and that its proof be added to Appendix A. > > Simple entailment lemma. S simple-entails E iff there is a graph > that can be derived from S by the application of the simple > entailment rules that is a supergraph of E. (Proof in Appendix A.) >This lemma requires that the simple entailment rules be augmented to allow >vvv in rule se1 and bbb in rule se2 to be a blank node. See above. > >9b/ Section 7.2 does not provide an adequate syntactic characterization of >RDF entailment. > >SUGGESTION: I suggest that Section 7.2 be augmented by the following >change to the RDF entailment lemma and that its proof in Appendix A be >modified accordingly. > > RDF entailment lemma. S rdf-entails E if and only if ... and which > is a supergraph of E. (Proof in Appendix A.) > > >9c/ Section 7.3 does not provide an adequate syntactic characterization of >RDF entailment. > >SUGGESTION: I suggest that Section 7.3 be augmented by adding the >following lemma and providing a proof for it in Appendix A. > > RDFS consistency lemma. S is rdfs-consistent if and only if it is > not possible to derive a supergraph of a graph of the following > form from S plus the RDF and RDFS axiomatic triples by the > application of the simple, RDF, and RDFS entailment rules > > uuu vvv rrr^^rdfs:XMLLiteral . > vvv rdfs:range www . > www rdfs:subClassOf rdfs:Literal . > > where rrr is a non-well formed XML literal. (Proof in Appendix A.) > >I believe that this is a correct characterization of RDFS consistency but >this would have to be shown in the proof. > >SUGGESTION: I suggest that Section 7.3 be augmented by the following >change to the RDFS entailment lemma and that its proof in Appendix A be >modified accordingly. > > RDFS entailment lemma. If S is rdfs-consistent then S rdfs-entails > E if and only if ... and which is a supergraph of E. (Proof in > Appendix A.) Thanks for your suggestions. 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@ihmc.us http://www.ihmc.us/users/phayesReceived on Monday, 29 September 2003 13:17:11 UTC

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