+ 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{}. It constitutes a reimplementation of the core
+ features of the pioneering \OmegaAnts{} system in the new \wss{}
+ framework.
+
+ A running prototype has been implemented as part of the
+ \helm{} project \cite{helm}
+ 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.
+
+ Future works comprise the implementation of new features and tutors, and
+ the embedding of the system in larger test cases. For instance, one
+ interesting case study would be interfacing a CAS as Maple to the
+ \hbugs{} broker, developing at the same time a tutor that implements the
+ Field tactic of Coq, which proves the equality of two expressions in an
+ abstract field by reducing both members to the same normal form. CASs can
+ produce several compact normal forms, which are particularly informative
+ to the user and that may suggest how to proceed in a proof. Unfortunately,
+ CASs do not
+ provide any certificate about the correctness of the simplification. On
+ the contrary, the Field tactic certifies the equality of two expressions,
+ but produces normal forms that are hardly a simplification of the original
+ formula. The benefits for the CAS would be obtained by using the Field tutor
+ to certify the CAS simplifications, proving that the Field normal form
+ of an expression is preserved by the simplification.
+ More advanced tutors could exploit the CAS to reduce the
+ goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
+ certify the simplification according to the skeptical approach.
+
+ We have many plans for further developing both the \hbugs{} architecture and
+ our prototype. 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 commands to narrow the choice of tactics available to the user.
+ This approach could be interesting especially for novice users, but requires
+ the client to increase their level of trust in the other actors.
+
+ We plan also to add some rating mechanism to the architecture. A first
+ improvement in this direction could be distinguishing between hints that, when
+ 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:
+ since the new goals can be false, the user can be forced later on to
+ backtrack.
+
+ 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 \cite{ring}.
+
+ We are also considering to follow the \OmegaAnts{} path adding
+ ``recursion'' to the system so that the proof status resulting from the
+ application of old hints are cached somewhere and could be used as a starting
+ 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 want
+ it to be really usable by novices. In particular, a critical issue
+ is avoiding continuous distractions for the user determined by the hints
+ that are asynchronously 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 proof-assistants users. So far, only the tutor
+ that is interfaced with the \helm{} Search-Engine has effectively increased
+ the productivity of experts users. The usefulness of the tutors developed for
+ beginners, instead, need further assessment.