]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/calculemus-2003/referaggio_hbugs.txt
Patch to delift withdrawn.
[helm.git] / 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 ------------------------------------------------------------------------------