1 ? when you show the examples of using your queries, please provide
2 the link to the web interface of Whelp where the readers can check
3 these examples themselves.
4 ? some bibliography items ([5], [7], [12]) do not seem to be mentioned
5 anywhere in the text of the article.
6 ? please explain the content of the files returned by the queries
7 in the form 'cic:/<some-path>.con', so that the readers who are
8 less familiar with Coq can also understand it.
10 ? Another annoying aspect of the paper is that while the approach is
11 claimed to be general, most of the problems the authors talk about (this
12 is particularly true in the conclusion) seems to be system specific (Coq).
15 The approach of the meta-data is mostly presented as an alternative
16 to other approaches. It seems very good at ruling out irrelevant
17 theorems but a bit unprecise. We believe the approaches are just
18 complementary. Applying first the meta-data and then some more
19 semantic technique seems an interesting and effective way of
20 producing more pertinent results.
23 In the case of Elim instead of trying to figure out if a theorem is
24 an elimination theorem it would be much simpler to let the author of
25 the theorem to indicate it explicitly (for example with a comment
26 schema as in Javadoc).
27 In general, it seems a valuable feature to let database developers
28 contribute to the meta-data generation.
31 An interesting question this section raises is how people name (or
32 should name) their theorems in a formal development. It seems that
33 your meta-data approach indicates an effective naming schema.
35 ROBA FATTA (+) O IGNORATA (=):
37 + if there exist -> if there exists
38 = The real contribution of the paper is difficult to assess since a fair amount
39 of what is presented here has already been published somewhere else. If the
40 paper is finally accepted we strongly encourage the authors to restructure
41 the paper and focus more on what is really new in what they present.