X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Freferaggio_hbugs_short.txt;h=8cd16d934a8e3492458de021bf7350a963c05ee1;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=61a896f47645412205c36d35e4a5b36a669e78c8;hpb=3b1f8c2a9042fd9aae286262f167272b91016d8e;p=helm.git diff --git a/helm/papers/calculemus-2003/referaggio_hbugs_short.txt b/helm/papers/calculemus-2003/referaggio_hbugs_short.txt index 61a896f47..8cd16d934 100644 --- a/helm/papers/calculemus-2003/referaggio_hbugs_short.txt +++ b/helm/papers/calculemus-2003/referaggio_hbugs_short.txt @@ -1,88 +1,8 @@ -// 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") +ROBA SOSTANZIALE: -/ 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 +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 - 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 @@ -95,17 +15,15 @@ Possibili spunti: 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 + 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. -