and beginners (who can learn from it).
\end{abstract}
-\section{Introduction}
+\section{Introduction\ednote{Zack: attualmente sembra che posto ne abbiamo: se
+la situazione non muta un 10 righe su \helm{} possiamo metterle, non tanto per
+la conferenza quanto per i posteri}}
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
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},
+ \oldpart 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
\wss{}.
+ \begin{newpart}Since the \emph{Declaration of Linz}, the MONET Consortium
+ \cite{MONET}, is working on the development of a framework, based on the
+ \wss{}/brokers approac, aimed at providing a set of software tools for the
+ advertisement and the discovery of mathematical \wss{}.\end{newpart}
%CSC This framework turns out to be strongly based on both \wss{} and brokers.
Several groups have already developed \wss{} providing both computational and
A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
which provided similar functionalities to the
\Omegapp{} proof-planner \cite{Omega}. The main architectural difference
- between \hbugs{} and \OmegaAnts{} is that the latter is based on a
+ between \hbugs{} and \OmegaAnts{} are 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}.
domain.
}
-\section{Architecture}
+\section{An \hbugs{} Bird'S Eye View\ednote{Zack: sono in vena di boiate
+stasera!}}
\label{architecture}
\myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
An \hbugs{} client is a software component able to produce \emph{proof
status} and to consume \emph{hints}.
- \ednote{Zack: "status" ha il plurale? CSC: no}
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 requirements exist on the proof status, but there should be an
agreement on its format between clients and tutors. An hint is a
- representation\ednote{non c'\'e un sinonimo pi\'u carino?}
+ representation\ednote{CSC: non c'\'e un sinonimo pi\'u carino? Zack: l'unico
+ decente sembra essere nuovamente "suggestion"}
of a step that can be performed in order to proceed in an
incomplete proof. Usually it represents a reference to a tactic available
on some proof assistant along with an instantiation for its formal
parameters. More structured hints can also be used: an hint can be
as complex as a whole proof-plan.
- 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)
- and as requesters (to submit new status). Clients
+ \myincludegraphics{interfaces}{t}{8cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
+ \wss{} interfaces}
+
+ Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
+ provider and requester, see \ednote{Zack: va bene "see"?, "cfr" credo sia
+ solo italiano ...} Fig. \ref{interfaces}.
+ They act as providers for the broker (to receive hints)
+ and as requesters (to submit new status) \ednote{Zack: non manca il "for"
+ anche per i requesters?}. Clients
additionally use broker service to know which tutors are available and to
subscribe to one or more of them.
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
+ \hbugs{} clients act as MONET clients and ask brokers 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 behave as \ws{}
- providers and requesters for \emph{both} clients and tutors.
+ Brokers are the key actors of the \hbugs{} architecture since they
+ act as intermediaries between clients and tutors. They behave as \wss{}
+ providers and requesters for \emph{both} clients and tutors, see Fig.
+ \ref{interfaces}.
With respect to client, a broker act as \ws{} provider, receiving the
proof status and forwarding it to one or more tutors.
by requesting computations (\emph{musings} in \hbugs{} terminology) on
status received by clients and by stopping already late but still
ongoing \musings{}
- \ednote{Sta frase va comunque riscritta perch\'e non si capisce una mazza}.
+ \ednote{CSC: Sta frase va comunque riscritta perch\'e non si capisce una
+ mazza. Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo commento
+ sulla utilita'/quantita' delle figure ...}
Additionally brokers keep track of available tutors and clients
subscriptions.
\hbugs{} tutors act as MONET services.
-\section{Implementation details}
+\section{Implementation's Highlights}
\label{implementation}
\ednote{Zack: l'aspetto grafico di questa parte e' un po' peso, possiamo
aggiungere varie immagini volendo, e.g.: schema dei thread di un tutor, sample
code di un tutor generato automaticamente}
-\ednote{Zack: ho cambiato idea riguardo a questa parte, mettere la lista delle
-interfacce di client/broker/... mi sembrava sterile e palloso. Di conseguenza ho
-messo i punti chiave dell'implementazione, dimmi cosa te ne pare ...}
In this section we present some of the most relevant implementation details of
the \hbugs{} architecture.
broker to send him an unique identifier and its base URI as a
\ws{}. After the registration, the client can use broker's
\texttt{List\_tutors} method to get a list of available tutors.
- Eventually\ednote{CSC: Vuoi veramente dire eventually qui?} the
+ Eventually\ednote{CSC: Vuoi veramente dire eventually qui? Zack: si, prima o
+ poi lo faranno ...} the
client can subscribe to one or more of these using broker's \emph{Subscribe}
method. Clients can also unregister from brokers using
\texttt{Unregister\_client} method.
just to update the \musings{} registry.
Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
- stai delirando?} is able to know, at each time,
+ stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
+ ovviamente ...} is able to know, at each time,
which \musings{} are in execution on which tutor. This peculiarity is
exploited by the broker on invocation of Status method. Receiving a new
status from the client imply indeed that the previous status no longer
received, the thread actually running them is killed freeing its
resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
ricordo male al problema dell'uccisione dei thread. Ora o si spiega
- il motivo di questa architettura o si glissa/bluffa.}
+ il motivo di questa architettura o si glissa/bluffa. Zack: cosa ti sembra
+ delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...}
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.
figuring out where the lemmas could have been stored in the library.
\end{enumerate}
-\section{???}
+\section{Conclusions and Future Work\ednote{Zack: ho scritto la parte "future
+work"}}
\label{conclusions}
+ We have many plan for further developing both the \hbugs{} architecture and
+ our prototype implementing them. Interesting results could be obtained
+ augmenting the informative content of each suggestion. We can for example
+ modify the broker so that also negative results are sent back to the client.
+ Those negative suggestions could be reflected in the user interface by
+ deactivating command narrowing the choice of tactics available to the user.
+ This approach could be interesting expecially for novice users, but require
+ the client to trust other actors a bit more than in the current approach.
+
+ We plan also to add some rating mechanism to the architecture. A first
+ improvement in this direction could be to distinguish between hints that, when
+ applied, are able to close one or more\ednote{Zack: e' possibile?} goals and
+ tactics that doesn't. Other heuristics and/or measures could be added to rate
+ hints and show them to the user in a particular order: an interesting one
+ could be a measure that try to minimize the size of the generated proof,
+ privileging therefore non-overkilling solutions\ednote{Zack: qua se vuoi ti
+ puoi pure auto-citare, cosa vuoi di piu'?}
+
+ We are also considering to follow the \OmegaAnts{} path more closely adding
+ ``recursion'' to the system so that proof status resulting from the
+ application of old hints are cached somewhere and could be used as a starting
+ point for new hint searches. Tough the approach is interesting, it moves the
+ focus closer to automatic theorem proving and we are considering if its worth
+ the effort given the increasing availability of automation in proof
+ assistants' tactics.
+
+ Even if not strictly part of the \hbugs{} architecture, the graphical user
+ interface (GUI) of our prototype needs a lot of improvement if we would like
+ it to be usable by novices.\ednote{Zack: la parte della GUI non ci sta molto
+ bene, sembra che vogliamo fare soldi vendendo HBugs ... forse va solo
+ formulata meglio ...}
+
+ Finally we hardly believe that \wss{} such our brokers and tutors could be
+ used also as components uncoupled from our client, exploiting their
+ capabilities is for example possible to develop a web-based proof assistant
+ demonstrative application. In order to widen even more their accessibility we
+ plan to write MONET descriptions \ednote{Zack: controllare se esiste un
+ termine piu' preciso} of the \wss{} offered by \hbugs{} actors. For the same
+ reasons we plan also to add support for Mathematical Object Managers both for
+ store and retrieve proof status.
\begin{thebibliography}{01}
projects / helm.git / commitdiff