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{\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}
 
 
 \title{Brokers and Web-Services for Automatic Deduction: a Case Study}
 


@@ -59,10 +61,10 @@
 \end{abstract}
 
 \section{Introduction}
 \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
   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
   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
   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
   "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
   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},
 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.
 \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
 \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?}
   \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}
   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
  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
  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}
 
  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
   \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
   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
   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.
 
   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
   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}.
 
   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.
   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
   
 \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.
 
   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
   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.
 }
 
   domain.
 }