From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 May 2003 13:31:42 +0000 (+0000)
Subject: Other references added.
X-Git-Tag: submitted~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a24d8528dc2241006a2a5eebca607bef96b1868a

Other references added.
An old part removed.
---

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 9e3db7894..78f614de2 100644
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -87,11 +87,14 @@
   advertisement and the discovery of mathematical \wss{}.
   %CSC This framework turns out to be strongly based on both \wss{} and brokers.
 
-  Several groups have already developed \wss{} providing both computational and
-  reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
-  dalle conferenze calculemus}: the formers are implemented on top of
+  Several groups have already developed software bus and
+  services\footnote{The most part of these systems predate the development of
+  \wss. Those systems whose development is still active are slowly being
+  reimplemented as \wss.} providing both computational and reasoning
+  capabilities \cite{ws1,ws2,ws3,ws4}: the formers are implemented on top of
   Computer Algebra Systems; the latters provide interfaces to well-known
-  theorem provers. Proof-planners, proof-assistants, CAS and
+  theorem provers.
+  Proof-planners, proof-assistants, CAS and
   domain-specific problem solvers are natural candidates to be client of these
   services.  Nevertheless, so far the number of examples in the literature has
   been extremely low and the concrete benefits are still to be assessed.
@@ -125,25 +128,6 @@
   Sect. \ref{tutors} is an overview of the tutors that have been implemented.
   As usual, the paper ends with the conclusions and future works.
   
-\oldpart
-{CSC:  Non so se/dove mettere queste parti.
- Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
-       non e' molto utile, ma la seconda sugli usi tipici di proof assistant
-       come ws client si}
-{
-  Despite of that the proof assistant case seems to be well suited to
-  investigate the usage of many different mathematical \wss{}. Indeed: most
-  proof assistants are still based on non-client/server architectures, are
-  application-centric instead of document-centric, offer a scarce level of
-  automation leaving entirely to the user the choice of which macro (usually
-  called \emph{tactic}) to use in order to make progress in a proof.
-
-  The average proof assistant can be, for example, a client of a \ws{}\
-  interfacing a specific or generic purpose theorem prover, or a client of a
-  \ws{} interfacing a CAS to simplify expressions in a particular mathematical
-  domain.
-}
-
 \section{An \hbugs{} Bird'S Eye View}
 \label{architecture}
   \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
@@ -692,6 +676,14 @@ we have investigated three classes of tutors:
  Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
  \url{http://www.w3.org/TR/wsdl12-bindings/}
 
+\bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
+ Deduction Systems via the Logic Broker Architecture. In Proceedings
+ of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
+
+\bibitem{ws3} O. Caprotti. Symbolic Evaluator Service. Project Report of
+ the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
+ Austria, May 2002.
+
 \bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
  Mathematical Knowledge Management in HELM. In Annals of Mathematics and
  Artificial Intelligence, 38(1): 27--46, May 2003.
@@ -731,6 +723,13 @@ we have investigated three classes of tutors:
 \bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
  dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
 
+\bibitem{ws4} J. Zimmer and L. Dennis. Inductive Theorem Proving and
+ Computer Algebra in the MathWeb Software Bus. In Proceedings of the 10th
+ CALCULEMUS Symposium 2002, 3--5 July 2002.
+
+\bibitem{ws2} R. Zippel. The MathBus. In Workshop on Internet Accessible
+ Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
+
 \end{thebibliography}
  
 \end{document}