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).