]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/calculemus-2003/referaggio_hbugs_short.txt
More notation here and there.
[helm.git] / helm / papers / calculemus-2003 / referaggio_hbugs_short.txt
1 ROBA SOSTANZIALE:
2
3 YES:  H-Bugs is simply an adaptation of a subset of the functionalities
4       of O-Ants to the MONET web-services/brokers approach.
5
6 (ii)  In the conclusion the authors admit that their work is rather
7       preliminary and that a real integration into the
8       MONET architecture is still missing. In  addition the following critique
9       should be addressed: The representations for  proof status  and  hints
10       in the brokers and tutors are client specific. What level of abstraction
11       is thus reached by the approach over the peculiarities and
12       representation formats of the client systems? Is it a feature that for
13       each client-tutor
14       combination new representation formats have to be agreed upon and
15       provided? I was actually hoping to find some more client independent
16       modelings of tutor services. Since this seems to be not an issue it
17       raises the question what the benefits of a modeling of H-Bugs within the
18       MONET web-services / brokers approach generally can be?
19       
20       Where is the abstraction that is typically achieved in service/broker
21       modelings (see second paragraph in the Introduction)?
22
23       If there is no abstraction
24       achieved over the representation format for proofs used by HELM what
25       again is the difference to O-Ants: the main application of O-Ants
26       operates on the OMEGA proof datastructure; however it has been claimed
27       that the O-Ants architecture is independent from it and this has
28       recently been illustrated by applications of the system in other
29       settings (e.g. paper at MKM-1001, Festschrift-Siekmann).