+}
+\begin{newpart}{riformulo}
+ 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
+ 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
+ literature has been extremely low and the concrete benefits are still
+ to be assessed.\ednote{A questo punto bisogna venire al
+ sodo prima che il lettore passi al caff\'e}
+\end{newpart}
+
+ 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
+ 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
+ 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.
+ Both the broker and the tutors are instances of the homonymous entities of
+ the MONET framework.