helm/papers/whelp/referaggi/RIASSUNTO_CRITICHE_E_SUGGERIMENTI

   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.
   9
  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).
  13
  14 ? Section 4:
  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.
  21
  22 ? Section 5.3:
  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.
  29
  30 ? Section 5.4:
  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.
  34
  35 ROBA FATTA (+) O IGNORATA (=):
  36
  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.