helm/papers/calculemus-2003/referaggio_hbugs_short.txt

   1 // certainly non-optimal presentation and structure. There are also quite many
   2    typos
   3 // The work presented in this paper, however, is still in a preliminary stage
   4    and convincing, novel scientific aspects are hardly identifiable
   5    (vedi sotto "Possibili spunti")
   6
   7 / include a short session on how you envision using the services from
   8   outside of H-Bugs, even outside of a proof-assistant environment if possible.
   9 / how to integrate into H-Bugs for instance a computer algebra package as
  10   tutor for ring simplification or for computing witnesses
  11 / the registration aspect seems quite different.  In my understanding, this
  12   broker is a a very specialized planner in MONET terminology: it has internal
  13   knowledge of the domain area of proof assistants (it knows the formats of
  14   proof status and hints).  The all architecture of H-Bugs has certain aspects
  15   that can be identified in the MONET architecture but it lacks the generality.
  16 / English: lots of errors in the third-person conjugation of verbs (missing s),
  17   please correct them - I will not list all of them. Try to have a native
  18   English speaker read the paper.
  19 / Use Section instead of Sect.
  20   On receipt of an hint  ->  Upon receival of a hint
  21   An hint  ->  A hint  (everywhere!)
  22   An usage  ->  A usage  (check www.bartleby.com/64)
  23   reply the work  ->  replay/replicate? the work
  24
  25
  26 - About the broker, in w3c terminology one has connectors, components and
  27   gateways, wouldn't you say that the broker is a gateway?
  28 - You compare H-Bugs to the MONET architecture, why? Please shortly give a
  29   motivation. One may wonder why not comparing to Omega instead.
  30 - Sessions 2 and 4 are too long, there are many repetitions.
  31
  32 - Page 12: in the Calculemus tradition, intelligent tutors like CAS can be
  33   integrated with a skeptical approach. You must check former Calculemus
  34   proceedings for references.
  35
  36
  37 / Page 9, do all tutors have the same interface? This is quite a uniform
  38   environment, which is not typical of a web service architecture. All the
  39   H-Bugs brokers provide a uniform H-Bugs broker interface.
  40
  41
  42 ### (CRITICHE FEROCI)
  43 page 2: ... are natural candidates ...
  44
  45 In MathWeb, for instance, many of the mentioned systems are not just
  46 candidates for being clients, they are clients.
  47
  48 page 2: ... number of examples in the literature has been extremely low and
  49 the concrete benefits are still to be assessed.
  50
  51 MathWeb, for instance, has been extensively used in case studies (where
  52 several thousands of subproblems have been attacked by MathWeb service
  53 systems).
  54
  55 What is the novel aspect of your case study? What do I learn?
  56
  57 page 2: The citation for MathWeb is not very well chosen. There is a system
  58 +description at CADE 2002 which is probably better suited.  (This may also hold
  59 +for other citations.)
  60
  61 Possibili spunti:
  62
  63 (i)   H-Bugs is an improved realization of the O-Ants approach; the
  64       architecture of H-Bugs is superior to that of O-Ants and H-Bugs
  65       provides more or at least some improved functionalities.
  66 (ii)  H-Bugs is simply an adaptation of a subset of the functionalities
  67       of O-Ants to the MONET web-services/brokers approach.
  68 (iii) The paper presents a case study with H-Bugs that gives novel insights or
  69       provides new evidence for the usefulness of systems like H-Bugs and
  70       O-Ants. (Because the title says  ...: a case study  this is what the
  71       reader first expects).
  72
  73 (i)   H-Bugs functionalities still appear to be a rather small subset of
  74       O-Ants functionalities. A proper comparison of functionalities is
  75       unfortunately missing. Example: H-Bugs does still present the
  76       hints in unsorted lists. Taking into account that the number of hints
  77       (especially when it comes to suggestions of parameters) can easily
  78       become very large, a heuristically structured presentation (which the
  79       authors mention as future work) seems to be a crucial requirement for
  80       such a system.
  81       There are many more aspects of O-Ants which seem to be not yet
  82       addressed in H-Bugs  A proper comparison of the H-Bugs functionalities
  83       and architecture
  84       with the O-Ants functionalities and architecture should be given if the
  85       authors contribution is meant to be (i).
  86 (ii)  In the conclusion the authors admit that their work is rather
  87       preliminary and that a real integration into the
  88       MONET architecture is still missing. In  addition the following critique
  89       should be addressed: The representations for  proof status  and  hints
  90       in the brokers and tutors are client specific. What level of abstraction
  91       is thus reached by the approach over the peculiarities and
  92       representation formats of the client systems? Is it a feature that for
  93       each client-tutor
  94       combination new representation formats have to be agreed upon and
  95       provided? I was actually hoping to find some more client independent
  96       modelings of tutor services. Since this seems to be not an issue it
  97       raises the question what the benefits of a modeling of H-Bugs within the
  98       MONET web-services / brokers approach generally can be? Where is the
  99       abstraction that is typically achieved in service/broker modelings (see
 100       second paragraph in the Introduction)? If there is no abstraction
 101       achieved over the representation format for proofs used by HELM what
 102       again is the difference to O-Ants: the main application of O-Ants
 103       operates on the OMEGA proof datastructure; however it has been claimed
 104       that the O-Ants architecture is independent from it and this has
 105       recently been illustrated by applications of the system in other
 106       settings (e.g. paper at MKM-1001, Festschrift-Siekmann).
 107 (iii) A proper evaluation of the case study is missing and the authors
 108       themselves mention proper assessment as future work. The claim that the
 109       tutor embodying the HELM-Search-Engine has effectively increased the
 110       productivity  of users is not at all justified in the paper.
 111