\newcommand{\myincludegraphics}[5]{
\begin{figure}[#2]
\begin{center}
- \includegraphics[width=#3]{XFIG-EPS/#1.eps}
+ \includegraphics[width=#3]{eps/#1.eps}
\caption[#4]{#5}
\label{#1}
\end{center}
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
- 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
- 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.
+ 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 \ednote{zack: buhm! :-P} 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},
-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.
-\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 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
- 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}
+ Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
+ following the guidelines \ednote{guidelines non e' molto appropriato, dato che
+ il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers
+ approach, is 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.
+
+ 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 themselves 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.
In this paper we present an architecture, namely \hbugs{}, implementing a
\emph{suggestion engine} for the proof assistant developed on behalf of the
As usual, the paper ends with the conclusions and future works.
\oldpart
-{Non so se/dove mettere queste parti}
+{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
domain.
}
-\section{???}
+\section{Architecture}
\label{architecture}
+ \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
+
+ The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
+ different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
+ Each actor present one or more \ws{} interface to its neighbours \hbugs{}
+ actors.
+
+ In this section we will detail the role and requiremente of each kind of
+ actors and discuss about the correspondencies between them and the MONET
+ entities described in \cite{MONET-Overview}.
+
+ \paragraph{Clients}
+ An \hbugs{} client is a software component able to produce \emph{proof
+ status} and to consume \emph{hints}.
+
+ \ednote{"status" ha il plurale?}
+ A proof status is a representation of an incomplete proof and is supposed to
+ be informative enough to be used by an interactive proof assistant. No
+ additional requirement exists on the proof status, but there should be an
+ agreement on its format between clients and tutors. An hint is a
+ representation of a step that can be performed in order to proceed in an
+ incomplete proof. Usually it represents a tactic available on some proof
+ assistant along with instantiation of its parameters for tactics which
+ require them.
+
+ Clients act both as \ws{} provider and requester (using W3C's terminology
+ \cite{ws-glossary}). They act as providers for the broker (to receive hints)
+ ans as requesters again for the broker (to submit new status). Clients
+ additionally use broker service to know which tutors are available and to
+ subscribe to one or more of them.
+
+ Usually, when the role of client is taken by an interactive proof assistant,
+ new status are sent to the broker as soon as the proof change (e.g. when the
+ user applies a tactic or when a new proof is started) and hints are shown to
+ the user be the means of some effect in the user interface (e.g. popping a
+ dialog box or enlightening a tactic button).
+
+ \hbugs{} clients act as MONET clients and ask broker to provide access to a
+ set of services (the tutors). \hbugs{} has no actors corresponding to MONET's
+ Broker Locating Service (since the client is supposed to know the URI of at
+ least one broker) and Mathematical Object Manager (since proof status are
+ built on the fly and not stored).
+
+ \paragraph{Brokers}
+ \hbugs{} brokers are the key actors of the \hbugs{} architecture since they
+ act as intermediaries between clients and tutors. They act both as \ws{}
+ provider and requester \emph{both} for clients and tutors.
+
+ With respect to client, a broker act as \ws{} provider receiving status and
+ forwarding them to one or more tutors. They act as \ws{} requester sending
+ hints to client as soon as they are available from tutors.
+
+ With respect to tutors, the \ws{} provider role is accomplished by receiving
+ hints as soon as they are produced; the \ws{} requester one is accomplished
+ by requesting computations (\emph{musings} in \hbugs{} terminology) on status
+ received by clients and stopping out of date ongoing musings.
+
+ Additionally brokers keep track of available tutors and subscription of each
+ client.
+
+ \hbugs{} brokers act as MONET brokers implementing the following components:
+ Client Manager, Service Registry Manager (keeping track of available
+ tutors), Planning Manager (chosing the available tutors among the ones to
+ which the client is subscribed), Execution Manager. \ednote{non e' chiaro se
+ in monet le risposte siano sincrone o meno, se cosi' fosse dobbiamo
+ specificare che nel nostro caso non lo sono}
+
+ \paragraph{Tutors}
+ Tutors are software component able to consume proof status producing hints.
+ \hbugs{} doesn't specify by which means hints should be produced, tutors can
+ use any means necessary (heuristics, external theorem prover or CAS, ...).
+ The only requirement is that exists an agreement on the formats of proof
+ status and hints.
+
+ tutors act both as \ws{} providers and requesters for broker. As providers,
+ they wait for commands requesting to start a new musing on a given proof
+ status or to stop an old, out of date, musing. As requesters, they signal to
+ the broker the end of a musing along with its outcome (an hint in case of
+ success or a notification of failure).
+
+ \hbugs{} tutors act as MONET services.
\section{???}
\label{implementation}
projects / helm.git / commitdiff