helm/papers/calculemus-2003/referaggio_hbugs.txt

   1 Dear Claudio Sacerdoti Coen,
   2
   3 Thank you for your submission to Calculemus 2003.  We are pleased to inform
   4 you that your paper, titled
   5
   6 Brokers and Web-Services for Automatic Deduction: a Case Study
   7
   8 has been accepted as a full paper for publication in the Proceedings.
   9 Papers went through a rigorous reviewing process.  Each paper was
  10 reviewed by at least three program committee members and was discussed
  11 at the program committee meeting.
  12
  13 Full papers are limited to 12 pages. Your camera-ready paper is due on July
  14 15, 2003. In order to help you to prepare your final paper, you will find
  15 bellow the referees' report on your paper,
  16
  17 To submit your paper, revisit the Calculemus 2003 submission site at
  18
  19 http://www-calfor.lip6.fr/home/rr/public_html/Calculemus03/submit/submit/
  20
  21 go to step 3, and use the login name and password that you received for
  22 submiting the abstract and paper
  23
  24 You will need to submit both a file containing the source(s) and a final file
  25 in pdf or postscript format.
  26
  27 In the following reports "A" means strong accept, "B" means weak accept,"C"
  28 means weak reject and "D" means strong reject. As of reviewers "X" means
  29 expert, "Y" means knowledgeable and "Z" means informed outsider.
  30
  31 We remind you that a special issue of the London Mathematical Journal
  32 dedicated to Calculemus 2003 will have a deadline around november.
  33
  34 Congratulations on having your paper accepted. We look forward to
  35 seeing you in Roma.
  36
  37 Sincerely,
  38
  39 Therese Hardin, Renaud Rioboo
  40 Calculemus 2003 PC Chairs
  41
  42 ----------
  43 Version number: 2
  44 Paper number: 12
  45 Reviewer number: XX
  46 1 - Classification: A
  47 2 - Your overall expertise on the areas of this paper: X
  48 3 - Contribution type: both a research paper and an experience report.
  49 4 - Summary of the paper:
  50 ------------------------------------------------------------------------------
  51
  52 The paper presents a collection of web services each implementing an automated
  53 deduction tactic. The services are coordinated by a broker able dispatch a
  54 proof status and collect hints back from the services. This architecture has
  55 been implemented in H-Bugs, an environment for supporting proof development.
  56
  57 ------------------------------------------------------------------------------
  58 6 - Comments for the author(s):
  59 ------------------------------------------------------------------------------
  60
  61 The topic of the paper is quite interesting: a shift from user-oriented
  62 software development to a web-service oriented software is probably on its way
  63 and will naturally occur. For the Calculemus core goal of integrating
  64 mechanized reasoning and symbolic computation, this shift is very important
  65 because it will provide off-the-shelf methods that can be used to improve the
  66 problem solving activity (whether it is computing or proving). Your list of
  67 potential clients to these services (on page 2) gives a glance into this
  68 vision.  I rated the paper with the full accept because the topic is important
  69 for Calculemus but I think the paper needs careful revision. I strongly
  70 encourage you to elaborate the paper including a short session on how you
  71 envision using the services from outside of H-Bugs, even outside of a
  72 proof-assistant environment if possible.
  73
  74 Also you should discuss how to integrate into H-Bugs for instance a computer
  75 algebra package as tutor for ring simplification or for computing witnesses...
  76
  77
  78
  79 ------------------------------------------------------------------------------
  80
  81 7 - Points in favour or against:
  82 ------------------------------------------------------------------------------
  83 Comments:
  84
  85 You compare H-Bugs to the MONET architecture, why? Please shortly give a
  86 motivation. One may wonder why not comparing to Omega instead. As you notice
  87 in the conclusion, the lack of ontologies to describe the the problems solved
  88 by your services confine these services to the H-Bug broker. Also, the
  89 registration aspect seems quite different.  In my understanding, this broker
  90 is a a very specialized planner in MONET terminology: it has internal
  91 knowledge of the domain area of proof assistants (it knows the formats of
  92 proof status and hints).  The all architecture of H-Bugs has certain aspects
  93 that can be identified in the MONET architecture but it lacks the generality.
  94 About the broker, in w3c terminology one has connectors, components and
  95 gateways, wouldn't you say that the broker is a gateway?  Sessions 2 and 4 are
  96 too long, there are many repetitions.
  97
  98
  99 Page 9, do all tutors have the same interface? This is quite a uniform
 100 environment, which is not typical of a web service architecture. All the
 101 H-Bugs brokers provide a uniform H-Bugs broker interface.
 102
 103 Page 12: in the Calculemus tradition, intelligent tutors like CAS can be
 104 integrated with a skeptical approach. You must check former Calculemus
 105 proceedings for references.
 106
 107 English: lots of errors in the third-person conjugation of verbs (missing s),
 108 please correct them - I will not list all of them. Try to have a native
 109 English speaker read the paper.
 110
 111 Use Section instead of Sect.
 112  On receipt of an hint  ->  Upon receival of a hint
 113  An hint  ->  A hint  (everywhere!)
 114  An usage  ->  A usage  (check www.bartleby.com/64)
 115  reply the work  ->  replay/replicate? the work
 116
 117 ------------------------------------------------------------------------------
 118 Version number: 5
 119 Paper number: 12
 120 Reviewer number: XX
 121 1 - Classification: C
 122 2 - Your overall expertise on the areas of this paper: X
 123 3 - Contribution type: an experience report.
 124 4 - Summary of the paper:
 125 ------------------------------------------------------------------------------
 126 The paper presents the system H-Bugs which consists of a (MONET-)broker and
 127 several (MONET-)web-services supporting the generation of hints in interactive
 128 theorem proving. The motivation  of H-Bugs and its functionalities are very
 129 closely related to the O-Ants framework developed in Saarbruecken and
 130 Birmingham; the authors call O-Ants a precursor of their system.
 131 ------------------------------------------------------------------------------
 132 6 - Comments for the author(s):
 133 ------------------------------------------------------------------------------
 134 It appears very interesting and useful to adapt the O-Ants approach to
 135 the MONET web-services/brokers framework. The work presented in this paper,
 136 however, is still in a preliminary stage and convincing, novel scientific aspects are hardly identifiable. This may be caused to a large extend by the certainly non-optimal presentation and structure. There are also quite many typos.
 137
 138
 139
 140 The main problem of the paper in my opinion is that the authors do not
 141 provide a clear picture on what their intellectual achievement and contribution actually is. Let us discuss some options:
 142
 143 (i)   H-Bugs is an improved realization of the O-Ants approach; the
 144       architecture of H-Bugs is superior to that of O-Ants and H-Bugs
 145       provides more or at least some improved functionalities.
 146 (ii)  H-Bugs is simply an adaptation of a subset of the functionalities
 147       of O-Ants to the MONET web-services/brokers approach.
 148 (iii) The paper presents a case study with H-Bugs that gives novel insights or
 149       provides new evidence for the usefulness of systems like H-Bugs and
 150       O-Ants. (Because the title says  ...: a case study  this is what the
 151       reader first expects).
 152
 153 The presentation addresses all three aspects a bit but fails
 154 to provide convincing arguments for either of them:
 155
 156 (i)   H-Bugs functionalities still appear to be a rather small subset of
 157       O-Ants functionalities. A proper comparison of functionalities is
 158       unfortunately missing. Example: H-Bugs does still present the
 159       hints in unsorted lists. Taking into account that the number of hints
 160       (especially when it comes to suggestions of parameters) can easily
 161       become very large, a heuristically structured presentation (which the
 162       authors mention as future work) seems to be a crucial requirement for
 163       such a system.
 164       There are many more aspects of O-Ants which seem to be not yet
 165       addressed in H-Bugs  A proper comparison of the H-Bugs functionalities
 166       and architecture
 167       with the O-Ants functionalities and architecture should be given if the
 168       authors contribution is meant to be (i).
 169 (ii)  In the conclusion the authors admit that their work is rather
 170       preliminary and that a real integration into the
 171       MONET architecture is still missing. In  addition the following critique
 172       should be addressed: The representations for  proof status  and  hints
 173       in the brokers and tutors are client specific. What level of abstraction
 174       is thus reached by the approach over the peculiarities and
 175       representation formats of the client systems? Is it a feature that for
 176       each client-tutor
 177       combination new representation formats have to be agreed upon and
 178       provided? I was actually hoping to find some more client independent
 179       modelings of tutor services. Since this seems to be not an issue it
 180       raises the question what the benefits of a modeling of H-Bugs within the
 181       MONET web-services / brokers approach generally can be? Where is the
 182       abstraction that is typically achieved in service/broker modelings (see
 183       second paragraph in the Introduction)? If there is no abstraction
 184       achieved over the representation format for proofs used by HELM what
 185       again is the difference to O-Ants: the main application of O-Ants
 186       operates on the OMEGA proof datastructure; however it has been claimed
 187       that the O-Ants architecture is independent from it and this has
 188       recently been illustrated by applications of the system in other
 189       settings (e.g. paper at MKM-1001, Festschrift-Siekmann).
 190 (iii) A proper evaluation of the case study is missing and the authors
 191       themselves mention proper assessment as future work. The claim that the
 192       tutor embodying the HELM-Search-Engine has effectively increased the
 193       productivity  of users is not at all justified in the paper.
 194
 195
 196 Some further remarks:
 197
 198 page 2: ... are natural candidates ...
 199
 200 In MathWeb, for instance, many of the mentioned systems are not just
 201 candidates for being clients, they are clients.
 202
 203 page 2: ... number of examples in the literature has been extremely low and
 204 the concrete benefits are still to be assessed.
 205
 206 MathWeb, for instance, has been extensively used in case studies (where
 207 several thousands of subproblems have been attacked by MathWeb service
 208 systems).
 209
 210
 211 What is the novel aspect of your case study? What do I learn?
 212
 213
 214 page 2: The citation for MathWeb is not very well chosen. There is a system description at CADE 2002 which is probably better suited.  (This may also hold for other citations.)
 215
 216
 217
 218 ------------------------------------------------------------------------------
 219
 220 7 - Points in favour or against:
 221 ------------------------------------------------------------------------------
 222 Pro: The work is definitely very relevant.
 223 Contra: Preliminary work stage, presentation and structure of paper is non-optimal, scientific contribution not clearly identifiable
 224 ------------------------------------------------------------------------------
 225 Version number: 1
 226 Paper number: 12
 227 Reviewer number: XX
 228 1 - Classification: A
 229 2 - Your overall expertise on the areas of this paper: X
 230 3 - Contribution type: both a research paper and an experience report.
 231 4 - Summary of the paper:
 232 ------------------------------------------------------------------------------
 233 The paper presents a distributed proof suggestion/theorem provring system
 234 based on W3C-style web services. The approach is closely patterned after the
 235 OMEGA-Ants system. The main (and important) difference is that it is
 236 distributed over the web. This is a great case study for web services, and
 237 quite a technological feat.
 238
 239 The paper is well-written, and explains the system in sufficient detail.
 240 ------------------------------------------------------------------------------
 241 6 - Comments for the author(s):
 242 ------------------------------------------------------------------------------
 243 What I would really like to see is a wrapper for the OMEGA Ants system that
 244 exports some of its Agengs as H-Bugs services, so that we can have O/H-hybrid
 245 populations of agents. Or of course an OMEGA Ants interpreter (the OAgents are
 246 given somewhat declaratively, if I recall) so that they can be exported as web
 247 services.
 248 ------------------------------------------------------------------------------
 249
 250 7 - Points in favour or against:
 251 ------------------------------------------------------------------------------
 252 not filled in
 253 ------------------------------------------------------------------------------