Dear Claudio Sacerdoti Coen, Thank you for your submission to Calculemus 2003. We are pleased to inform you that your paper, titled Brokers and Web-Services for Automatic Deduction: a Case Study has been accepted as a full paper for publication in the Proceedings. Papers went through a rigorous reviewing process. Each paper was reviewed by at least three program committee members and was discussed at the program committee meeting. Full papers are limited to 12 pages. Your camera-ready paper is due on July 15, 2003. In order to help you to prepare your final paper, you will find bellow the referees' report on your paper, To submit your paper, revisit the Calculemus 2003 submission site at http://www-calfor.lip6.fr/home/rr/public_html/Calculemus03/submit/submit/ go to step 3, and use the login name and password that you received for submiting the abstract and paper You will need to submit both a file containing the source(s) and a final file in pdf or postscript format. In the following reports "A" means strong accept, "B" means weak accept,"C" means weak reject and "D" means strong reject. As of reviewers "X" means expert, "Y" means knowledgeable and "Z" means informed outsider. We remind you that a special issue of the London Mathematical Journal dedicated to Calculemus 2003 will have a deadline around november. Congratulations on having your paper accepted. We look forward to seeing you in Roma. Sincerely, Therese Hardin, Renaud Rioboo Calculemus 2003 PC Chairs ---------- Version number: 2 Paper number: 12 Reviewer number: XX 1 - Classification: A 2 - Your overall expertise on the areas of this paper: X 3 - Contribution type: both a research paper and an experience report. 4 - Summary of the paper: ------------------------------------------------------------------------------ The paper presents a collection of web services each implementing an automated deduction tactic. The services are coordinated by a broker able dispatch a proof status and collect hints back from the services. This architecture has been implemented in H-Bugs, an environment for supporting proof development. ------------------------------------------------------------------------------ 6 - Comments for the author(s): ------------------------------------------------------------------------------ The topic of the paper is quite interesting: a shift from user-oriented software development to a web-service oriented software is probably on its way and will naturally occur. For the Calculemus core goal of integrating mechanized reasoning and symbolic computation, this shift is very important because it will provide off-the-shelf methods that can be used to improve the problem solving activity (whether it is computing or proving). Your list of potential clients to these services (on page 2) gives a glance into this vision. I rated the paper with the full accept because the topic is important for Calculemus but I think the paper needs careful revision. I strongly encourage you to elaborate the paper including a short session on how you envision using the services from outside of H-Bugs, even outside of a proof-assistant environment if possible. Also you should discuss how to integrate into H-Bugs for instance a computer algebra package as tutor for ring simplification or for computing witnesses... ------------------------------------------------------------------------------ 7 - Points in favour or against: ------------------------------------------------------------------------------ Comments: You compare H-Bugs to the MONET architecture, why? Please shortly give a motivation. One may wonder why not comparing to Omega instead. As you notice in the conclusion, the lack of ontologies to describe the the problems solved by your services confine these services to the H-Bug broker. Also, 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. About the broker, in w3c terminology one has connectors, components and gateways, wouldn't you say that the broker is a gateway? Sessions 2 and 4 are too long, there are many repetitions. 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. 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. 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 ------------------------------------------------------------------------------ Version number: 5 Paper number: 12 Reviewer number: XX 1 - Classification: C 2 - Your overall expertise on the areas of this paper: X 3 - Contribution type: an experience report. 4 - Summary of the paper: ------------------------------------------------------------------------------ The paper presents the system H-Bugs which consists of a (MONET-)broker and several (MONET-)web-services supporting the generation of hints in interactive theorem proving. The motivation of H-Bugs and its functionalities are very closely related to the O-Ants framework developed in Saarbruecken and Birmingham; the authors call O-Ants a precursor of their system. ------------------------------------------------------------------------------ 6 - Comments for the author(s): ------------------------------------------------------------------------------ It appears very interesting and useful to adapt the O-Ants approach to the MONET web-services/brokers framework. The work presented in this paper, 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. The main problem of the paper in my opinion is that the authors do not provide a clear picture on what their intellectual achievement and contribution actually is. Let us discuss some options: (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). The presentation addresses all three aspects a bit but fails to provide convincing arguments for either of them: (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. Some further remarks: 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.) ------------------------------------------------------------------------------ 7 - Points in favour or against: ------------------------------------------------------------------------------ Pro: The work is definitely very relevant. Contra: Preliminary work stage, presentation and structure of paper is non-optimal, scientific contribution not clearly identifiable ------------------------------------------------------------------------------ Version number: 1 Paper number: 12 Reviewer number: XX 1 - Classification: A 2 - Your overall expertise on the areas of this paper: X 3 - Contribution type: both a research paper and an experience report. 4 - Summary of the paper: ------------------------------------------------------------------------------ The paper presents a distributed proof suggestion/theorem provring system based on W3C-style web services. The approach is closely patterned after the OMEGA-Ants system. The main (and important) difference is that it is distributed over the web. This is a great case study for web services, and quite a technological feat. The paper is well-written, and explains the system in sufficient detail. ------------------------------------------------------------------------------ 6 - Comments for the author(s): ------------------------------------------------------------------------------ What I would really like to see is a wrapper for the OMEGA Ants system that exports some of its Agengs as H-Bugs services, so that we can have O/H-hybrid populations of agents. Or of course an OMEGA Ants interpreter (the OAgents are given somewhat declaratively, if I recall) so that they can be exported as web services. ------------------------------------------------------------------------------ 7 - Points in favour or against: ------------------------------------------------------------------------------ not filled in ------------------------------------------------------------------------------