Minor improvements in the introduction.

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index f3fee974894bb265d7165f24ad065e0d6fb36f5b..8c72523507f749cb2d0fec6db641562b5c27316c 100644 (file)
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -22,6 +22,8 @@
 \newcommand{\wss}{Web-Services}
 \newcommand{\hbugs}{H-Bugs}
 \newcommand{\helm}{HELM}
+\newcommand{\Omegapp}{$\Omega$mega}
+\newcommand{\OmegaAnts}{$\Omega$mega-Ants}
 
 \title{Brokers and Web-Services for Automatic Deduction: a Case Study}
 
@@ -59,10 +61,10 @@
 \end{abstract}
 
 \section{Introduction}
-  The \ws\ approach at software development seems to be a working solution for
+  The \ws{} approach at software development seems to be a working solution for
   getting rid of a wide range of incompatibilities between communicating
   software applications. W3C's efforts in standardizing related technologies
-  grant longevity and implementations availability for frameworks based on \wss\
+  grant longevity and implementations availability for frameworks based on \wss{}\
   for information exchange. As a direct conseguence, the number of such
   frameworks is increasing and the World Wide Web is moving from a disorganized
   repository of human-understandable HTML documents to a disorganized repository
@@ -76,10 +78,10 @@
   This lack of organization along with the huge amount of documents available,
   have posed not a few problems for data location. If this limitation could be
   overcome using heuristic-based search engine for HTML pages, a satisfying
-  solution has yet to be found for \ws\ location \ednote{location non mi piace, ma
+  solution has yet to be found for \ws{} location \ednote{location non mi piace, ma
   "localization" e' anche peggio, "retrieval"?}. A promising architecture seems
   to be the use of \emph{brokers}, which access point (usually an URI) is known
-  by the potential clients or by \emph{registries}, to which the \wss\ subscribe
+  by the potential clients or by \emph{registries}, to which the \wss{} subscribe
   to publish their functionalities.
 }
 \begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale
@@ -91,26 +93,26 @@ The standard solution is providing a further level of stable services
 applications to access a wide variety of services and abstract over them.
 
 Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
-following the guidelines of the \wss/brokers approach, is
+following the guidelines of the \wss{}/brokers approach, is
 \end{newpart}
   working on the development of a framework aimed at providing a set of software
   tools for the advertisement and discovering of mathematical web services.
-%CSC This framework turns out to be strongly based on both \wss\ and brokers.
+%CSC This framework turns out to be strongly based on both \wss{} and brokers.
 \oldpart
 {Hhhmm. Chiaro il punto, ma CAS and Theorem Prover related web-services non
  \'e molto preciso.}
 {
   Several examples of CAS (Computer Algebra System) and Theorem Prover related
-  \wss\ have been shown to be useful and to fit well in the MONET Architecture
+  \wss{} have been shown to be useful and to fit well in the MONET Architecture
   \ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?}
-  the set of \wss\ related to Proof Assistants tends to be ... rather ...
+  the set of \wss{} related to Proof Assistants tends to be ... rather ...
   empty!\ednote{gia' mi immagino il tuo commento: BUHM! :-)}
 }
 \begin{newpart}{riformulo}
- Several groups have already developed \wss\ providing both computational
+ Several groups have already developed \wss{} providing both computational
  and reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori
- carini dalle conferenze calculemus}: the first ones are implemented
- on top of Computer Algebra Systems; the last ones provide interfaces to
+ carini dalle conferenze calculemus}: 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
  domain-specific problem solvers are natural candidates to be client
  of these services. Nevertheless, so far the number of examples in the
@@ -119,42 +121,42 @@ following the guidelines of the \wss/brokers approach, is
  sodo prima che il lettore passi al caff\'e}
 \end{newpart}
 
-  In this paper we present an architecture, namely \hbugs\, implementing a
+  In this paper we present an architecture, namely \hbugs{}, implementing a
   \emph{suggestion engine} for the proof assistant developed on behalf of the
-  \helm\ project. We provide several \wss (called \emph{tutors}) able to
+  \helm{} project. We provide several \wss{} (called \emph{tutors}) able to
   suggest possible ways to proceed in a proof. The tutors are orchestrated
-  by a broker (a \ws\ itself) that is able to distribute a proof
+  by a broker (a \ws{} itself) that is able to distribute a proof
   status from a client (the proof-assistant) to the tutors;
   each tutor try to make progress in the proof and, in case
-  of success, notify the client that shows and \emph{hint} to the user.
+  of success, notify the client that shows an \emph{hint} to the user.
   Both the broker and the tutors are instances of the homonymous entities of
   the MONET framework.
 
-  A precursor of \hbugs is the $\Omega$-Ants project \cite{???},
+  A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
   which provided similar functionalities to the
-  Omega proof-planner \cite{Omega}. The main architectural difference
-  between \hbugs and $\Omega$-Ants is that the latter is based on a
-  black-board architecture and it is not implemented using \wss and
+  \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
+  between \hbugs{} and \OmegaAnts{} is that the latter is based on a
+  black-board architecture and it is not implemented using \wss{} and
   brokers. Other differences will be detailed in Sect. \ref{conclusions}.
 
-  In Sect. \ref{architecture} we present the architecture of \hbugs.
+  In Sect. \ref{architecture} we present the architecture of \hbugs{}.
   Further implementation details are given in Sect. \ref{implementation}.
   Sect. \ref{tutors} is an overview of the tutors that have been implemented.
-  Finally, the last section is left for the conclusions and future works.
+  As usual, the paper ends with the conclusions and future works.
   
 \oldpart
 {Non so se/dove mettere queste parti}
 {
   Despite of that the proof assistant case seems to be well suited to
-  investigate the usage of many different mathematical \wss. Indeed: most proof
+  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\
+  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
+  \ws{} interfacing a CAS to simplify expressions in a particular mathematical
   domain.
 }