From: Claudio Sacerdoti Coen Date: Fri, 27 Jun 2003 12:34:44 +0000 (+0000) Subject: ... X-Git-Tag: camera_ready~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3b1f8c2a9042fd9aae286262f167272b91016d8e ... --- diff --git a/helm/papers/calculemus-2003/referaggio_hbugs.txt b/helm/papers/calculemus-2003/referaggio_hbugs.txt new file mode 100644 index 000000000..8899c4ea2 --- /dev/null +++ b/helm/papers/calculemus-2003/referaggio_hbugs.txt @@ -0,0 +1,253 @@ +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 +------------------------------------------------------------------------------ diff --git a/helm/papers/calculemus-2003/referaggio_hbugs_short.txt b/helm/papers/calculemus-2003/referaggio_hbugs_short.txt new file mode 100644 index 000000000..61a896f47 --- /dev/null +++ b/helm/papers/calculemus-2003/referaggio_hbugs_short.txt @@ -0,0 +1,111 @@ +// 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. +