1 // certainly non-optimal presentation and structure. There are also quite many
3 // The work presented in this paper, however, is still in a preliminary stage
4 and convincing, novel scientific aspects are hardly identifiable
5 (vedi sotto "Possibili spunti")
7 / include a short session on how you envision using the services from
8 outside of H-Bugs, even outside of a proof-assistant environment if possible.
9 / how to integrate into H-Bugs for instance a computer algebra package as
10 tutor for ring simplification or for computing witnesses
11 / the registration aspect seems quite different. In my understanding, this
12 broker is a a very specialized planner in MONET terminology: it has internal
13 knowledge of the domain area of proof assistants (it knows the formats of
14 proof status and hints). The all architecture of H-Bugs has certain aspects
15 that can be identified in the MONET architecture but it lacks the generality.
16 / English: lots of errors in the third-person conjugation of verbs (missing s),
17 please correct them - I will not list all of them. Try to have a native
18 English speaker read the paper.
19 / Use Section instead of Sect.
20 On receipt of an hint -> Upon receival of a hint
21 An hint -> A hint (everywhere!)
22 An usage -> A usage (check www.bartleby.com/64)
23 reply the work -> replay/replicate? the work
26 - About the broker, in w3c terminology one has connectors, components and
27 gateways, wouldn't you say that the broker is a gateway?
28 - You compare H-Bugs to the MONET architecture, why? Please shortly give a
29 motivation. One may wonder why not comparing to Omega instead.
30 - Sessions 2 and 4 are too long, there are many repetitions.
32 - Page 12: in the Calculemus tradition, intelligent tutors like CAS can be
33 integrated with a skeptical approach. You must check former Calculemus
34 proceedings for references.
37 / Page 9, do all tutors have the same interface? This is quite a uniform
38 environment, which is not typical of a web service architecture. All the
39 H-Bugs brokers provide a uniform H-Bugs broker interface.
43 page 2: ... are natural candidates ...
45 In MathWeb, for instance, many of the mentioned systems are not just
46 candidates for being clients, they are clients.
48 page 2: ... number of examples in the literature has been extremely low and
49 the concrete benefits are still to be assessed.
51 MathWeb, for instance, has been extensively used in case studies (where
52 several thousands of subproblems have been attacked by MathWeb service
55 What is the novel aspect of your case study? What do I learn?
57 page 2: The citation for MathWeb is not very well chosen. There is a system
58 +description at CADE 2002 which is probably better suited. (This may also hold
59 +for other citations.)
63 (i) H-Bugs is an improved realization of the O-Ants approach; the
64 architecture of H-Bugs is superior to that of O-Ants and H-Bugs
65 provides more or at least some improved functionalities.
66 (ii) H-Bugs is simply an adaptation of a subset of the functionalities
67 of O-Ants to the MONET web-services/brokers approach.
68 (iii) The paper presents a case study with H-Bugs that gives novel insights or
69 provides new evidence for the usefulness of systems like H-Bugs and
70 O-Ants. (Because the title says ...: a case study this is what the
71 reader first expects).
73 (i) H-Bugs functionalities still appear to be a rather small subset of
74 O-Ants functionalities. A proper comparison of functionalities is
75 unfortunately missing. Example: H-Bugs does still present the
76 hints in unsorted lists. Taking into account that the number of hints
77 (especially when it comes to suggestions of parameters) can easily
78 become very large, a heuristically structured presentation (which the
79 authors mention as future work) seems to be a crucial requirement for
81 There are many more aspects of O-Ants which seem to be not yet
82 addressed in H-Bugs A proper comparison of the H-Bugs functionalities
84 with the O-Ants functionalities and architecture should be given if the
85 authors contribution is meant to be (i).
86 (ii) In the conclusion the authors admit that their work is rather
87 preliminary and that a real integration into the
88 MONET architecture is still missing. In addition the following critique
89 should be addressed: The representations for proof status and hints
90 in the brokers and tutors are client specific. What level of abstraction
91 is thus reached by the approach over the peculiarities and
92 representation formats of the client systems? Is it a feature that for
94 combination new representation formats have to be agreed upon and
95 provided? I was actually hoping to find some more client independent
96 modelings of tutor services. Since this seems to be not an issue it
97 raises the question what the benefits of a modeling of H-Bugs within the
98 MONET web-services / brokers approach generally can be? Where is the
99 abstraction that is typically achieved in service/broker modelings (see
100 second paragraph in the Introduction)? If there is no abstraction
101 achieved over the representation format for proofs used by HELM what
102 again is the difference to O-Ants: the main application of O-Ants
103 operates on the OMEGA proof datastructure; however it has been claimed
104 that the O-Ants architecture is independent from it and this has
105 recently been illustrated by applications of the system in other
106 settings (e.g. paper at MKM-1001, Festschrift-Siekmann).
107 (iii) A proper evaluation of the case study is missing and the authors
108 themselves mention proper assessment as future work. The claim that the
109 tutor embodying the HELM-Search-Engine has effectively increased the
110 productivity of users is not at all justified in the paper.