X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Freferaggio_hbugs_short.txt;fp=helm%2Fpapers%2Fcalculemus-2003%2Freferaggio_hbugs_short.txt;h=0000000000000000000000000000000000000000;hp=8cd16d934a8e3492458de021bf7350a963c05ee1;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/papers/calculemus-2003/referaggio_hbugs_short.txt b/helm/papers/calculemus-2003/referaggio_hbugs_short.txt
deleted file mode 100644
index 8cd16d934..000000000
--- a/helm/papers/calculemus-2003/referaggio_hbugs_short.txt
+++ /dev/null
@@ -1,29 +0,0 @@
-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).