--- /dev/null
+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
+------------------------------------------------------------------------------
--- /dev/null
+// 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.
+
projects / helm.git / commitdiff