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

Date: Fri, 8 Nov 2002 14:09:51 +0100

To: phayes@ai.uwf.edu, www-rdf-comments@w3.org

Message-ID: <OF54AA7E9A.6EB17CCB-ONC1256C6A.004CA10C-C1256C6B.0048837E@diamond.philips.com>

Date: Fri, 8 Nov 2002 14:09:51 +0100

To: phayes@ai.uwf.edu, www-rdf-comments@w3.org

Message-ID: <OF54AA7E9A.6EB17CCB-ONC1256C6A.004CA10C-C1256C6B.0048837E@diamond.philips.com>

Better late then never, I hope. Yesterday I saw the "Nondraft" at [1] of the new version of the RDF model theory document that is underway. I have some comments which are hopefully considered useful. The first two comments question the correctness of proofs; the other comments are small corrections/editorial suggestions. (Section numbers refer to [1].) - RDF closure lemma: since the definition of the set IP has been changed (it is now part of the definition of a simple interpretation), the last part of the proof of this lemma does not apply anymore: the set IEXT(I(aaa)) can no longer be assumed to be nonempty. (I fully support the change of the definition of IP, and considered the old version of this definition to be a "weak spot" in the document.) - There seems to be a problem with the proof of the second anonymity lemma. Consider the sentence "Since E is lean, it contains no other triples of the form S1 P1 O' or S2 P2 O'." This is true, when O' is assumed to be a name. However, E may contain two other triples S1 P1 _:x3 and S2 P2 _:x3. In this case, the last part of the proof does not apply. - 1.5: paragraph starting with "For example,": replace <1,2> by <1,1> - 3.1: example: it should be IR = {1,2,T,P} instead of {1,2,T} - 3.3: The introduction of the set IC looks a little circular, and can be made smoother (when I first read this, I had to stop for some time at this point). Namely: the mapping ICEXT is defined from classes to extensions (so the set of classes IC is assumed to be already there, although it is not explicitly specified) and subsequently, in the table, IC is described in terms of ICEXT. In my view, the going would become smoother when the explicit definition of IC, IC := {x in IR : <x, I(rdfs:Class)> in IEXT(I(rdf:type))}, is given before the definition of ICEXT : IC -> P(IR) given in the text. -2: definition of entailment. The central case of the document (S entails E where S is a set of RDF graphs and E is an RDF graph) could be understood quicker by saying [I satisfies S => I satisfies E] and by adding one line to the table of 1.6: [If S is a set of RDF graphs, then I(S) = I(Merge S).] This definition case could be added to the first paragraph of 2; it is convenient to use this when following the proofs, for example. With the original text, the reader can deduce this from the first paragraph of 2, but it takes more unwinding (the word expression has to be matched with the word RDF graph, etc.) - I suggest to add to the merging lemma: S entails E iff Merge S entails E. At several places where the merging lemma is used (for example, in the proof of the interpolation lemma), this addition would make the use of this lemma instantaneous. - Just before the minimality lemma: "It is clear that if I satisfies E then a minimal satisfying [add: sub]interpretation exists with a vocabulary precisely..." (I guess this is what is meant. Without this addition, the assumption is not needed.) - proof of anonymity lemma 1: "otherwise" suggests that now the negation of the preceding will be used, but this is not the case. It would be better to say: Since..., E' contains a triple [add: s'p'o' obtained by replacing a blank node by a name in the triple spo from E, while s'p'o'] has no instances in E; otherwise, the triple spo would have had a proper instance in E. - Interpolation lemma. It would be helpful to add the following corollary explicitly: E does not entail E' iff E' is separable from E. In addition to the two lemmas mentioned, the if direction also uses the subgraph lemma. - RDF entailment lemma: second paragraph: it should be rdf-interpretation instead of rdfs-interpretation Herman ter Horst Philips Research [1] http://www.coginst.uwf.edu/~phayes/RDF%20Model%20Theory_Oct_draft.htmlReceived on Saturday, 9 November 2002 03:01:27 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 22:44:01 UTC
*