+RILEGGERE E CORREGGERE:
+
// 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.
+ROBA SOSTANZIALE:
-/ 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.)
+// 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")
Possibili spunti:
-(i) H-Bugs is an improved realization of the O-Ants approach; the
+NO: 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
+YES: 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
+HHMM: The paper presents a case study with H-Bugs that gives novel insights or
+NO 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
projects / helm.git / blobdiff