++++++++++++++++++++++++ Comments on KWeb D.2.5.8 == General == * Overfull lines in page headers and TOC, many overfull hboxes throughout paper * replace most occurrences of "paper" with "chapter" == Chapter 2 == * p.4 "The user can develop *its* programs" * p.5 Acknowledgements: (project) acknowledgements out of place here I guess * Fig. 2.2.1 has no lines in my PDF; this might be a TeXnical issue, since the paper version of this chapter has a diagram there. * p.7 top claims "Not allowing terms in the heads of rules is not a restriction [since they] can be rewritten (using a predicate eq defining equality)" It is not explained where this "eq" comes from (note that you cannot axiomatise eq in the given syntax without using terms in rule heads). * p.10 Theorem 2 uses notation "T^{H_{KKS}}" and its claim is that "there exists a program transformation T^{H_{KKS}}". The proof, however, does not define this thing but starts with "let P' = T^{H_{KKS}}(P)". It probably should be defined somewhere what T^{H_{KKS}} is. Later in the proof, some things are concluded "by definition of T" but a full-text search on capital T in the chapter did not reveal to me where this definition could be. Probably some of the properties assumed in the proof should rather be definitions. I do not think that the result is at risk, it is just hard to follow the proof. * p.14 the role querying can only work for *simple* roles (not mentioned) == Chapter 3 == The chapter is quite nice ... I could not find anything more severe than this ;): * "an Herbrand interpretation" not "a Herbrand interpretation" (it's a French name) == Chapter 4 == No major comments here either. * p.54 "msembership" * p.59 "SPARLQ" == Chapter 5 == * There are numerous smaller grammar/spelling issues, e.g. p.62 "compositional[ly] consistent", "allows them [to] be interpreted", "neighbors" vs. "neighbour", ... I cannot collect all those here, but language problems are significant in places (see e.g. last paragraph of p.63). * p.63, Def. 24, 2. has "Times" where there should have been "\times", same on p.65 bottom (2x) * Fig. 5.1 is missing completely in my PDF * p.65, after second paragraph: character encoding problem (?), compare http://iswc2007.semanticweb.org/papers/659.pdf * Table 5.1 refers to single interpretations, hence it should be "(not) satisfied" instead of "(not) satisfiable" * p.68 Theorem 35 *is* Lemma 34; same for Lemma 38/Lemma 39/Theorem 40 * p.68 Definition 36: "Let AO_i\in \mathbb{AO}_i" is superfluous; same in Definition 41 * p.69, Definition 37: (b) obsoletes (a) by Theorem 35 and Lemma 34 ... I stop collecting more such formalisation/presentation glitches now * p.70 bottom: "is a tuple T = T upx0 , N, E, L," TeX issue (there should be angular brackets, not another T), the problem occurs a lot in this section * Theorems 43/44 are not proven, and no pointer to external proofs is given. * p. 72/73 show various "\mathcal{T}extbf" that should be commands ++++++++++++++++++++++++