+++ /dev/null
-ROBA SOSTANZIALE:
-
-YES: H-Bugs is simply an adaptation of a subset of the functionalities
- of O-Ants to the MONET web-services/brokers approach.
-
-(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
- should be addressed: The representations for proof status and hints
- in the brokers and tutors are client specific. What level of abstraction
- is thus reached by the approach over the peculiarities and
- representation formats of the client systems? Is it a feature that for
- each client-tutor
- combination new representation formats have to be agreed upon and
- 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
- 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).
projects / helm.git / blobdiff