// certainly non-optimal presentation and structure. There are also quite many typos // The work presented in this paper, however, is still in a preliminary stage and convincing, novel scientific aspects are hardly identifiable (vedi sotto "Possibili spunti") / include a short session on how you envision using the services from outside of H-Bugs, even outside of a proof-assistant environment if possible. / how to integrate into H-Bugs for instance a computer algebra package as tutor for ring simplification or for computing witnesses / the registration aspect seems quite different. In my understanding, this broker is a a very specialized planner in MONET terminology: it has internal knowledge of the domain area of proof assistants (it knows the formats of proof status and hints). The all architecture of H-Bugs has certain aspects that can be identified in the MONET architecture but it lacks the generality. / English: lots of errors in the third-person conjugation of verbs (missing s), please correct them - I will not list all of them. Try to have a native English speaker read the paper. / Use Section instead of Sect. On receipt of an hint -> Upon receival of a hint An hint -> A hint (everywhere!) An usage -> A usage (check www.bartleby.com/64) reply the work -> replay/replicate? the work - About the broker, in w3c terminology one has connectors, components and gateways, wouldn't you say that the broker is a gateway? - You compare H-Bugs to the MONET architecture, why? Please shortly give a motivation. One may wonder why not comparing to Omega instead. - Sessions 2 and 4 are too long, there are many repetitions. - Page 12: in the Calculemus tradition, intelligent tutors like CAS can be integrated with a skeptical approach. You must check former Calculemus proceedings for references. / Page 9, do all tutors have the same interface? This is quite a uniform environment, which is not typical of a web service architecture. All the H-Bugs brokers provide a uniform H-Bugs broker interface. ### (CRITICHE FEROCI) page 2: ... are natural candidates ... In MathWeb, for instance, many of the mentioned systems are not just candidates for being clients, they are clients. page 2: ... number of examples in the literature has been extremely low and the concrete benefits are still to be assessed. MathWeb, for instance, has been extensively used in case studies (where several thousands of subproblems have been attacked by MathWeb service systems). What is the novel aspect of your case study? What do I learn? 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.) Possibili spunti: (i) H-Bugs is an improved realization of the O-Ants approach; the architecture of H-Bugs is superior to that of O-Ants and H-Bugs provides more or at least some improved functionalities. (ii) H-Bugs is simply an adaptation of a subset of the functionalities of O-Ants to the MONET web-services/brokers approach. (iii) The paper presents a case study with H-Bugs that gives novel insights or provides new evidence for the usefulness of systems like H-Bugs and O-Ants. (Because the title says ...: a case study this is what the reader first expects). (i) H-Bugs functionalities still appear to be a rather small subset of O-Ants functionalities. A proper comparison of functionalities is unfortunately missing. Example: H-Bugs does still present the hints in unsorted lists. Taking into account that the number of hints (especially when it comes to suggestions of parameters) can easily become very large, a heuristically structured presentation (which the authors mention as future work) seems to be a crucial requirement for such a system. There are many more aspects of O-Ants which seem to be not yet addressed in H-Bugs A proper comparison of the H-Bugs functionalities and architecture with the O-Ants functionalities and architecture should be given if the authors contribution is meant to be (i). (ii) In the conclusion the authors admit that their work is rather preliminary and that a real integration into the MONET architecture is still missing. In addition the following critique should be addressed: The representations for proof status and hints in the brokers and tutors are client specific. What level of abstraction is thus reached by the approach over the peculiarities and representation formats of the client systems? Is it a feature that for each client-tutor combination new representation formats have to be agreed upon and provided? I was actually hoping to find some more client independent modelings of tutor services. Since this seems to be not an issue it raises the question what the benefits of a modeling of H-Bugs within the MONET web-services / brokers approach generally can be? Where is the abstraction that is typically achieved in service/broker modelings (see second paragraph in the Introduction)? If there is no abstraction achieved over the representation format for proofs used by HELM what again is the difference to O-Ants: the main application of O-Ants operates on the OMEGA proof datastructure; however it has been claimed that the O-Ants architecture is independent from it and this has recently been illustrated by applications of the system in other settings (e.g. paper at MKM-1001, Festschrift-Siekmann). (iii) A proper evaluation of the case study is missing and the authors themselves mention proper assessment as future work. The claim that the tutor embodying the HELM-Search-Engine has effectively increased the productivity of users is not at all justified in the paper.