]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/whelp/referaggi/RIASSUNTO_CRITICHE_E_SUGGERIMENTI
removed papers that have been moved to the new "papers" repository
[helm.git] / helm / papers / whelp / referaggi / RIASSUNTO_CRITICHE_E_SUGGERIMENTI
diff --git a/helm/papers/whelp/referaggi/RIASSUNTO_CRITICHE_E_SUGGERIMENTI b/helm/papers/whelp/referaggi/RIASSUNTO_CRITICHE_E_SUGGERIMENTI
deleted file mode 100644 (file)
index 6b7c3a1..0000000
+++ /dev/null
@@ -1,41 +0,0 @@
-? 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.