X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Freferaggio_hbugs.txt;fp=helm%2Fpapers%2Fcalculemus-2003%2Freferaggio_hbugs.txt;h=0000000000000000000000000000000000000000;hp=8899c4ea206b8ba0ac914a118f68cc8c8625a428;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/papers/calculemus-2003/referaggio_hbugs.txt b/helm/papers/calculemus-2003/referaggio_hbugs.txt deleted file mode 100644 index 8899c4ea2..000000000 --- a/helm/papers/calculemus-2003/referaggio_hbugs.txt +++ /dev/null @@ -1,253 +0,0 @@ -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 -------------------------------------------------------------------------------