\institute{
Department of Computer Science\\
University of Bologna\\
- Via di Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
+ Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
\email{sacerdot@cs.unibo.it}
\and
Department of Computer Science\\
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 an \emph{hint} to the user.
- Both the broker and the tutors are instances of the homonymous entities of
- the MONET framework.
+ The broker is an instance of the homonymous entity of the MONET framework.
+ The tutors are MONET services. Another \ws (which is not described in this
+ paper and which is called Getter \cite{}) is used to locate and download
+ mathematical entities; the Getter plays the role of the Mathematical Object
+ Manager in the MONET framework.
A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
which provided similar functionalities to the
\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).
+ URI of at least one broker). The \hbugs{} client and tutors contact the
+ Getter (a MONET Mathematical Object Manager) to locate and retrieve
+ mathematical items in the HELM library. The proof status that are exchanged
+ by the \hbugs{} actors, instead, are built on the fly and are neither
+ stored nor are given an unique identifier (URI) to be managed by the
+ Getter.
\paragraph{Brokers}
Brokers are the key actors of the \hbugs{} architecture since they
\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}
+ which the client is subscribed), Execution Manager. The Service Manager
+ component is not required since the session handler, that identifies
+ a session between a service and a broker, is provided to the service by
+ the broker instead of being received from the service when it is
+ initialized. In particular, a session is identified by an unique identifier
+ for the client (its URL) and an unique identifier for the broker (its
+ URL).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i
+ multi-sessione. Ma mi sembra la strada che prenderemmo, no?}
+
+ The MONET architecture specification does not state explicitely whether
+ the service and broker answers can be asyncronous. Nevertheless, the
+ described information flow implicitly suggests a syncronous implementation.
+ On the contrary, in \hbugs{} every request is asyncronous: the connection
+ used by an actor to issue a query is immediately closed; when a service
+ produces an answer, it gives it back to the issuer by calling the
+ appropriate actor's method.
\paragraph{Tutors}
Tutors are software component able to consume proof status producing hints.
To test the productivity impact of intelligent tutors, we have implemented
a tutor that is interfaced with the HELM
- Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ Search-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
is able to look for every theorem in the distributed library that can
be applied to proceed in the proof. Even if the tutor deductive power
is extremely limited\footnote{We do not attempt to check if the new goals
figuring out where the lemmas could have been stored in the library.
\end{enumerate}
-\section{Conclusions and Future Work\ednote{Zack: ho scritto la parte "future
-work"}}
+\section{Conclusions and Future Work}
\label{conclusions}
+ In this paper we described a suggestion engine architecture for
+ proof-assistants: the client (a proof-assistant) sends the current proof
+ status to several distributed \wss (called tutors) that try to progress
+ in the proof and, in case of success, send back an appropriate hint
+ (a proof-plan) to the user. The user, that in the meantime was able to
+ reason and progress in the proof, is notified with the hints and can decide
+ to apply or ignore them. A broker is provided to decouple the clients and
+ the tutors and to allow the client to locate and invoke the available remote
+ services. The whole architecture is an instance of the MONET architecture
+ for Mathematical \wss.
+
+ A running prototype has been implemented as part of the HELM project \cite{}
+ and we already provide several tutors. Some of them are simple tutors that
+ try to apply one or more tactics of the HELM Proof-Engine, which is also
+ our client. We also have a much more complex tutor that is interfaced
+ with the HELM Search-Engine and looks for lemmas that can be directly applied.
+
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.
+ deactivating commands to narrow 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
+ applied, are able to completely close one or more goals and
+ tactics that progress in the proof by reducing one or more goals to new goals:
+ the new goals could be false and the proof can be closed only by backtraking.
+
+ 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'?}
+ privileging therefore non-overkilling solutions \cite{ring}.
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.
+ point for new hint searches. The approach is interesting, but it represents
+ a big shift towards automatic theorem proving: thus we must consider if it is
+ worth the effort given the increasing availability of automation in proof
+ assistants' tactics and the ongoing development of \wss{} based on
+ already existent and well developed theorem provers.
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.
+ it to be usable by novices. In particular, the user is too easily distracted
+ by the tutor's hints that are ``pushed'' to her.
+
+ Our \wss still lack a real integration in the MONET architecture,
+ since we do not provide the different ontologies to describe our problems,
+ solutions, queries and services. In the short term, completing this task
+ could provide a significative feedback to the MONET consortium and would
+ enlarge the current set of available MONET actors on the web. In the long
+ term, new more intelligent tutors could be developed on top of already
+ existent MONET \wss.
+
+ To conclude, \hbugs{} is a nice experiment meant to understand whether the
+ current \wss technology is mature enough to have a concrete and useful impact
+ on the daily work of users of proof-assistants. So far, only the tutor that
+ is interfaced with the HELM Search-Engine has effectively increased the
+ productivity of experts users. The usefullness of the tutors developed for
+ beginners, instead, need further assessment.
\begin{thebibliography}{01}
projects / helm.git / commitdiff