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