software applications. W3C's efforts in standardizing related technologies
grant longevity and implementations availability for frameworks based on \wss\
for information exchange. As a direct conseguence, the number of such
- frameworks in increasing and the World Wide Web is moving from a disorganized
+ frameworks is increasing and the World Wide Web is moving from a disorganized
repository of human-understandable HTML documents to a disorganized repository
of applications working on machine-understandable XML documents both for input
and output.
+\oldpart
+{Di effetto la prima fase. La seconda era troppo fuori-tema e dettagliata per
+ un abstract}
+{
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
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
to publish their functionalities.
+}
+\begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale
+dovrebbe essere una versione pi\'u fluida e leggera. Boh.}
+The big challenge for the next future is to provide stable and reliable
+services over this disorganized, unreliable and ever-evolving architecture.
+The standard solution is providing a further level of stable services
+(called \emph{brokers}) that behave as common gateway/address for client
+applications to access a wide variety of services and abstract over them.
- Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET} is
+Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
+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. This
- framework turns out to be strongly based on both \wss\ and brokers.
-
+ tools for the advertisement and discovering of mathematical web services.
+%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
\ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?}
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
+ 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.
+ A precursor of \hbugs is the $\Omega$-Ants 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
+ brokers. Other differences will be detailed in Sect. \ref{conclusions}.
+
+ 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.
+
+\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
assistants are still based on non-client/server architectures, are
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.
+}
- The Omega Ants project \ednote{date, autori e paperi}, developed before the
- \emph{\ws\ era}, enrich the Omega \cite{Omega} proof assistant with an
- architecture able to distribute subparts of a proof to agents (Ants)
- implemented as separate processes running on the same hosts of the proof
- assistant \ednote{controllare ...}.
-
- 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. This architecture is based on a set of \wss\ and a broker (a
- \ws\ itself) and is able to distribute a proof status from a client to several
- \emph{tutor}, each of them can try to make progress in the proof and, in case
- of success, notify the user sending him an \emph{hint}. Both the broker and
- the tutors are instances of the homonymous entities of the MONET framework.
% \section{Introduction}
% Since the development of the first proof-assistants based on the
projects / helm.git / commitdiff