]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
Patch to delift withdrawn.
[helm.git] / helm / papers / calculemus-2003 / hbugs-calculemus-2003.tex
1 \documentclass[runningheads]{llncs}
2 \pagestyle{headings}
3 \setcounter{page}{1}
4 \usepackage{graphicx}
5 \usepackage{amsfonts}
6
7 % \myincludegraphics{filename}{place}{width}{caption}{label}
8 \newcommand{\myincludegraphics}[5]{
9    \begin{figure}[#2]
10    \begin{center}
11    \includegraphics[width=#3]{eps/#1.eps}
12    \caption[#4]{#5}
13    \label{#1}
14    \end{center}
15    \end{figure}
16 }
17
18 %\usepackage[show]{ed}
19 %\usepackage{draftstamp}
20
21 \newcommand{\musing}{\texttt{musing}}
22 \newcommand{\musings}{\texttt{musings}}
23 \newcommand{\ws}{Web-Service}
24 \newcommand{\wss}{Web-Services}
25 \newcommand{\hbugs}{H-Bugs}
26 \newcommand{\helm}{HELM}
27 \newcommand{\Omegapp}{$\Omega$mega}
28 \newcommand{\OmegaAnts}{$\Omega$mega-Ants}
29
30 \title{Brokers and Web-Services for Automatic Deduction: a Case Study}
31
32 \author{
33  Claudio Sacerdoti Coen\thanks{Partially supported by `MoWGLI: Math on the Web, Get it by Logic and Interfaces', EU IST-2001-33562} \and
34  Stefano Zacchiroli\thanks{Partially supported by `MyThS: Models and Types for Security in Mobile Distributed Systems', EU FET-GC IST-2001-32617}}
35
36 \institute{
37   Department of Computer Science\\
38   University of Bologna\\
39   Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
40   \email{sacerdot@cs.unibo.it}
41   \and
42   Department of Computer Science\\
43   \'Ecole Normale Sup\'erieure\\
44   45, Rue d'Ulm, F-75230 Paris Cedex 05, FRANCE\\
45   \email{zack@cs.unibo.it}
46 }
47
48 \date{ }
49
50 \begin{document}
51 \sloppy
52 \maketitle
53
54 \begin{abstract}
55   We present a planning broker and several Web-Services for automatic deduction.
56   Each Web-Service implements one of the tactics usually available in
57   interactive proof-assistants. When the broker is submitted a ``proof status''
58   (an incomplete proof tree and a focus on an open goal) it dispatches the proof
59   to the Web-Services, collects the successful results, and send them back to
60   the client as ``hints'' as soon as they are available.
61   
62   In our experience this architecture turns out to be helpful both for
63   experienced users (who can take benefit of distributing heavy computations)
64   and beginners (who can learn from it).
65 \end{abstract}
66
67 \section{Introduction}
68   The \ws{} approach at software development seems to be a working solution for
69   getting rid of a wide range of incompatibilities between communicating
70   software applications. W3C's efforts in standardizing related technologies
71   grant longevity and implementations availability for frameworks based on
72   \wss{} for information exchange. As a direct consequence, the number of such
73   frameworks is increasing and the World Wide Web is moving from a disorganized
74   repository of human-understandable HTML documents to a disorganized repository
75   of applications working on machine-understandable XML documents both for input
76   and output.
77   
78   The big challenge for the next future is to provide stable and reliable
79   services over this disorganized, unreliable, and ever-evolving architecture.
80   The standard solution is to provide a further level of stable services (called
81   \emph{brokers}) that behave as common gateways/addresses for client
82   applications to access a wide variety of services and abstract over them.
83
84   Since the \emph{Declaration of Linz}, the MONET
85   Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}}
86   is working on the development of a framework, based on the
87   \wss{}/brokers approach, aimed at providing a set of software tools for the
88   advertisement and the discovery of mathematical \wss{}.
89   %CSC This framework turns out to be strongly based on both \wss{} and brokers.
90
91   Several groups have already developed software bus and
92   services\footnote{The most part of these systems predate the development of
93   \wss. Those systems whose development is still active are slowly being
94   reimplemented as \wss.} providing both computational and reasoning
95   capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of
96   Computer Algebra Systems; the second ones provide interfaces to well-known
97   theorem provers.
98   Proof-planners, proof-assistants, CASs and
99   domain-specific problem solvers are natural candidates to be clients of these
100   services.  Nevertheless, so far the number of examples in the literature has
101   been insufficient to fully assess the concrete benefits of the framework.
102
103   In this paper we present an architecture, namely \hbugs{}, implementing a
104   \emph{suggestion engine} for the proof assistant developed on behalf of the
105   \helm{}\footnote{Hypertextual Electronic Library of Mathematics,
106   \url{http://helm.cs.unibo.it}} project
107   \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to
108   suggest possible ways to proceed in a proof. The tutors are orchestrated
109   by a broker (a \ws{} itself) that is able to dispatch a proof
110   status from a client (the proof-assistant) to the tutors;
111   each tutor tries to make progress in the proof and, in case
112   of success, notifies the client that shows an \emph{hint} to the user.
113   The broker is an instance of the homonymous entity of the MONET framework.
114   The tutors are MONET services. Another \ws{} (which is not described in this
115   paper and which is called Getter \cite{zack}) is used to locate and download
116   mathematical entities; the Getter plays the role of the Mathematical Object
117   Manager of the MONET framework.
118
119   A precursor of \hbugs{} is the \OmegaAnts{} project
120   \cite{omegaants1,omegaants2}, which provided similar functionalities to the
121   \Omegapp{} proof-planner \cite{omega}. The main architectural difference
122   between \hbugs{} and \OmegaAnts{} is that the latter is based on a
123   black-board architecture and it is not implemented using \wss{} and
124   brokers.
125
126   In Sect. \ref{architecture} we present the architecture of \hbugs{}.
127   A usage session is shown in Sect. \ref{usage}.
128   Further implementation details are given in Sect. \ref{implementation}.
129   Sect. \ref{tutors} is an overview of the tutors that have been implemented.
130   As usual, the final section of this paper is devoted to conclusions and future works.
131   
132 \section{An \hbugs{} Bird's Eye View}
133 \label{architecture}
134   \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
135
136   The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
137   different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
138   Each actor presents one or more \ws{} interfaces to its neighbors \hbugs{}
139   actors.
140
141   In this section we detail the role and requirements of each kind of
142   actors and we discuss about the correspondences between them and the MONET
143   entities described in \cite{MONET-Overview}.
144   Due to lack of space, we cannot compare our framework to similar proposals, as
145   the older and more advanced \Omegapp{} system. The study of the
146   correspondences with MONET is well motivated by the fact that the MONET
147   framework is still under development and that our implementation is one of the
148   first experiments in \ws based distributed reasoning. On the other hand, a
149   comparison with \Omegapp{} would be less interesting since the functionalities we
150   provide so far are just a subset of the \OmegaAnts{} ones.
151
152   \paragraph{Clients}
153     An \hbugs{} client is a software component able to produce \emph{proof
154     status} and to consume \emph{hints}.
155
156     A proof status is a representation of an incomplete proof and is supposed to
157     be informative enough to be used by an interactive proof assistant. No
158     additional requirements exist on the proof status, but there should be an
159     agreement on its format between clients and tutors. A hint is an
160     encoding of a step that can be performed in order to proceed in an
161     incomplete proof. Usually it represents a reference to a tactic available
162     on some proof assistant along with an instantiation for its formal
163     parameters. Hints can also be more structured: a hint can be
164     as complex as a whole proof-plan.
165
166     Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
167     providers and requesters, see Fig. \ref{interfaces}.
168     They act as providers receiving hints from the broker; they act as
169     requesters submitting new status to the tutors.
170     Clients additionally use broker services to know which tutors are available
171     and to subscribe to one or more of them.
172
173     Usually, when the client role is taken by an interactive proof assistant,
174     new status are sent to the broker as soon as the proof change (e.g. when the
175     user applies a tactic or when a new proof is started); hints are shown to
176     the user by the means of some effects in the user interface (e.g. popping a
177     dialog box or enlightening a tactic button).
178
179     \hbugs{} clients act as MONET clients and ask brokers to provide access to a
180     set of services (the tutors). \hbugs{} has no actors corresponding to
181     MONET's Broker Locating Service (since the client is supposed to know the
182     URI of at least one broker). The \hbugs{} clients and tutors contact the
183     Getter (a MONET Mathematical Object Manager) to locate and retrieve
184     mathematical items from the \helm{} library.
185     The proof status that are exchanged
186     by the \hbugs{} actors, instead, are built on the fly and are neither
187     stored nor given an unique identifier (URI) to be managed by the
188     Getter.
189
190   \paragraph{Brokers}
191     \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
192      {\hbugs{} \wss{} interfaces}
193
194     Brokers are the key actors of the \hbugs{} architecture since they
195     act as intermediaries between clients and tutors. They behave as \wss{}
196     providers and requesters for \emph{both} clients and tutors, see Fig.
197     \ref{interfaces}.
198
199     With respect to the client, a broker acts as a \ws{} provider, receiving the
200     proof status and forwarding it to one or more tutors.
201     It also acts as a \ws{} requester sending
202     hints to the client as soon as they are available from the tutors.
203
204     With respect to the tutors, the \ws{} provider role is accomplished by
205     receiving hints as soon as they are produced; as a requester, it is
206     accomplished by asking for computations (\emph{musings} in \hbugs{}
207     terminology) on status received by clients and by stopping already late but
208     still ongoing \musings{}.
209
210     Additionally brokers keep track of available tutors and clients
211     subscriptions.
212
213     \hbugs{} brokers act as MONET brokers implementing the following components:
214     Client Manager, Service Registry Manager (keeping track of available
215     tutors), Planning Manager (choosing the available tutors among the ones to
216     which the client is subscribed), Execution Manager. The Service Manager
217     component is not required since the session handler, that identifies
218     a session between a service and a broker, is provided to the service by
219     the broker instead of being received from the service when the session is
220     initialized. In particular, a session is identified by an unique identifier
221     for the client (its URL) and an unique identifier for the broker (its
222     URL).
223
224     Notice that \hbugs{} brokers have no knowledge of the domain area of
225     proof-assistants, nor they are able to interpret the messages that they
226     are forwarding. They are indeed only in charge of maintaining the
227     abstraction of several reasoning blackboards --- one for each client ---
228     of capacity one: a blackboard is created when the client submits a problem;
229     it is then ``shared'' by the client and all the tutors until the client
230     submits the next problem. For instance, replacing the client with a CAS and
231     all the tutors with agents implementing different resolution methods for
232     differential equations would not require any change in the broker. Notice
233     that all the tutors must expose the same interface to the broker.
234
235     The MONET architecture specification does not state explicitly whether the
236     service and broker answers can be asynchronous. Nevertheless, the
237     described information flow implicitly suggests a synchronous implementation.
238     On the contrary, in \hbugs{} every request is asynchronous: the connection
239     used by an actor to issue a query is immediately closed; when a service
240     produces an answer, it gives it back to the issuer by calling the
241     appropriate actor's method.
242
243   \paragraph{Tutors}
244     Tutors are software components able to consume proof status producing hints.
245     \hbugs{} does not specify by which means hints should be produced: tutors
246     can use any means necessary (heuristics, external theorem prover or CAS,
247     etc.). The only requirement is that there exists an agreement on the formats
248     of proof status and hints.
249
250     Tutors act both as \ws{} providers and requesters for the broker, see Fig.
251     \ref{interfaces}. As
252     providers, they wait for commands requesting to start a new \musing{} on
253     a given proof status or to stop an old, out of date, \musing{}. As
254     requesters, they signal to the broker the end of a \musing{} along with its
255     outcome (a hint in case of success or a failure notification).
256
257     \hbugs{} tutors act as MONET services.
258
259 \section{An \hbugs{} Session Example}
260 \label{usage}
261 In this section we describe a typical \hbugs{} session. The aim of the
262 session is to solve the following easy exercise:
263 \begin{exercise}
264 Let $x$ be a generic real number. Using the \helm{} proof-engine,
265 prove that
266 \begin{displaymath}
267 x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
268 \end{displaymath}
269 \end{exercise}
270
271 Let us suppose that the \hbugs{} broker is already running and that the
272 tutors already registered themselves to the broker.
273 When the user starts our proof-engine \texttt{gTopLevel}, the system registers itself to
274 the broker, that sends back the list of available tutors. By default,
275 \texttt{gTopLevel} notifies to the broker its intention of subscribing to every
276 tutor available. The user can always open a configuration window where she
277 is presented the list of available tutors and she can independently subscribe
278 and unsubscribe herself to each tutor.
279
280 \myincludegraphics{step1}{t}{12cm}{Example session.}
281   {Example session.}
282 %\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
283 % {Example session, snapshot 2.}
284
285 The user can now insert into the system the statement of the theorem and start
286 proving it. Let us suppose that the first step of the user is proving
287 that the denominator 2 is different from 0. Once that this technical result
288 is proven, the user must prove the goal shown in the upper right corner
289 of the window in background in Fig. \ref{step1}.
290
291 While the user is wondering how to proceed in the proof, the tutors are
292 trying to progress in the proof. After a while, the tutors' suggestions
293 start to appear in the lower part of the \hbugs{} interface window
294 (the topmost window in Fig. \ref{step1}). In this case, the tutors are able
295 to produce 23 hints. The first and not very useful hint suggests to proceed in
296 the proof by exchanging the two sides of the equality.
297 The second hint suggests to reduce both sides of the equality to their normal
298 form by using only reductions which are justified by the ring structure of the
299 real numbers; the two normal forms, though, are so different that the proof is
300 not really simplified.
301 All the residual 21 hints suggest to apply one lemma from the distributed
302 library of \helm{}. The user can look at the statement of any lemma by clicking
303 on its URI.
304
305 The user can now look at the list of suggestions and realize that a good one is
306 applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
307 members by the same scalar\footnote{Even if she does not receive the hint, the
308 user probably already knows that this is the right way to proceed. The
309 difficult part, accomplished by the hint, is guessing what is the name of the
310 lemma to apply.}.
311 Double-clicking on the hint automatically applies
312 the lemma, reducing the proof to closing three new goals. The first one asks
313 the user the scalar to use as an argument of the previous lemma; the second
314 one states that the scalar is different from 0; the third lemma (the main
315 one) asks to prove the equality between the two new members.
316 % is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
317 % the still unknown scalar argument, which can have only $H$ and $x$ as
318 % free variables.
319
320 The user proceeds by instantiating the scalar with the number 2. The
321 \texttt{Assumption} tutor now suggests to close the second goal (that
322 states that $2 \neq 0$) by applying the hypothesis $H$.
323 No useful suggestions, instead, are generated for the main goal
324 $2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
325 To proceed in the proof the user needs to simplify the
326 expression using the lemma $Rinv\_r\_simpl\_m$ that states that
327 $\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
328 suggesting simplifications, the user must find out this simplification by
329 himself. Once she founds it, the goal is reduced to proving that
330 $2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
331 \texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is
332 just one of the 22 hints that the user receives. It is the only hint that
333 does not open new goals, but the user right now does not have any way to know
334 that.} to the user how to complete the proof in one macrostep.
335
336 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
337 %    Comandi da dare a gTopLevel    %
338 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
339 % New proof:
340 %  !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
341 % Intros x H
342 % Apply  r_Rmult_mult
343 % 3: Apply H
344 % Simpl   (per fare unfold di Rdiv)
345 % Rewrite <-
346 %  (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
347 % Rewrite ->
348 %  (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
349 % *** Ring
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
351
352 \section{Implementation's Highlights}
353 \label{implementation}
354 In this section we present some of the most relevant implementation details of
355 the \hbugs{} architecture.
356
357
358   \paragraph{Proof status}
359     In our implementation of the \hbugs{} architecture we used the proof
360     assistant of the \helm{} project (codename \texttt{gTopLevel}) as an \hbugs{}
361     client. Thus we have implemented serialization/deserialization capabilities
362     for its internal status. In order to be able to describe \wss{} that
363     exchange status in WSDL using the XML Schema type system, we have chosen an
364     XML format as the target format for the serialization.
365
366 %    A schematic representation of the gTopLevel internal status is depicted in
367 %    Fig. \ref{status}.
368     Each proof is represented by a tuple of four elements:
369     \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
370
371 %    \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
372 %    status}
373
374     \begin{description}
375       \item[uri]: an URI chosen by the user at the beginning of the proof
376         process. Once (and if) proved, that URI will globally identify the term
377         inside the \helm{} library (given that the user decides to save it).
378       \item[thesis]: the ongoing proof thesis
379       \item[proof]: the current incomplete proof tree. It can contain
380         \emph{metavariables} (holes) that stands for the parts of the proof
381         that are still to be completed. Each metavariable appearing in the
382         tree references one element of the metavariables environment
383         (\emph{metasenv}).
384       \item[metasenv]: the metavariables environment is a list of
385         \emph{goals} (unproved conjectures).
386         In order to complete the proof, the user has to instantiate every
387         metavariable in the proof with a proof of the corresponding goal.
388         Each goal is identified by an unique identifier and has a context
389         and a type (the goal thesis). The context is a list of named
390         hypotheses (declarations and definitions). Thus the context and the goal
391         thesis form a sequent, which is the statement of the proof that will
392         be used to instantiate the metavariable occurrences.
393     \end{description}
394
395     Each of these information is represented in XML as described in
396     \cite{mowglicic}. Additionally, an \hbugs{} status carries the unique
397     identifier of the current goal, which is the goal the user is currently
398     focused on. Using this value it is possible to implement different client
399     side strategies: the user could ask the tutors to work on the goal
400     she is considering or to work on the other ``background'' goals.
401
402   \paragraph{Hints}
403     A hint in the \hbugs{} architecture should carry enough information to
404     permit the client to progress in the current proof. In our
405     implementation each hint corresponds to either one of the tactics available
406     to the user in gTopLevel (together with its actual arguments) or a set
407     of alternative suggestions (a list of hints).
408
409     For tactics that do not require any particular argument (like tactics that
410     apply type constructors or decision procedures)
411     only the tactic name is represented in the hint. For tactics that need
412     terms as arguments (for example the \texttt{Apply} tactic that apply a
413     given lemma) the hint includes a textual representation of them, using the
414     same representation used by the interactive proof assistant when querying
415     user for terms. In order to be transmitted between \wss{}, hints are
416     serialized in XML.
417
418     It is also possible for a tutor to return more hints at once,
419     grouping them in a particular XML element.
420     This feature turns out to be particularly useful for the
421     \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that
422     queries a lemma database and returns to the client a list of all lemmas that
423     could be used to complete the proof. This particular hint is encoded as a
424     list of \texttt{Apply} hints, each of them having one of the results as term
425     argument.
426
427     We would like to stress that the \hbugs{} architecture has no dependency
428     on either the hint or the status representation: the only message parts
429     that are fixed are those representing the administrative messages
430     (the envelopes in the \wss{} terminology). In particular, the broker can
431     manage at the same time several sessions working on different status/hints
432     formats. Of course, there must be an agreement between the clients
433     and the tutors on the format of the data exchanged.
434
435     In our implementation the client does not trust the tutors hints:
436     being encoded as references to available tactics imply
437     that an \hbugs{} client, at the receipt of a hint, simply try to replay
438     the work
439     done by a tutor on the local copy of the proof. The application of the hint
440     can even fail to type check and the client copy of the proof can be left
441     undamaged after spotting the error. Note, however, that it is still
442     possible to implement a complex tutor that looks for a proof doing
443     backtracking and that
444     send back to the client a hint whose argument is a witness (a trace) of
445     the proof found: the client applies the hint reconstructing (and checking
446     the correctness of) the proof from the witness, without having to
447     re-discover the proof itself.
448
449     An alternative implementation where the tutors are trusted would simply
450     send back to the client a new proof-status. Upon receiving the
451     proof-status, the client would just override its current proof status with
452     the suggested one. In the case of those clients which are implemented
453     using proof-objects (as the Coq proof-assistant, for instance), it is
454     still possible for the client to type-check the proof-object and reject
455     wrong hints. The systems that are not based on proof-objects
456     (as PVS, NuPRL, etc.), instead, must completely trust the new proof-status.
457     In this case the \hbugs{} architecture would need at least to be extended
458     with clients-tutors authentication.
459     
460   \paragraph{Registries}
461     Being central in the \hbugs{} architecture, the broker is also responsible
462     of housekeeping operations both for clients and tutors. These operations are
463     implemented using three different data structures called \emph{registries}:
464     clients registry, tutors registry and \musings{} registry.
465
466     In order to use the suggestion engine a client should register itself to the
467     broker and subscribe to one or more tutors. The registration phase is
468     triggered by the client using the \texttt{Register\_client} method of the
469     broker to send him an unique identifier and its base URI as a \ws{}. After
470     the registration, the client can use the \texttt{List\_tutors} method of the
471     broker to get a list of available tutors.  Eventually the client can
472     subscribe to one or more of these using the \texttt{Subscribe} method of the
473     broker. Clients can also unregister from brokers using
474     \texttt{Unregister\_client} method.
475
476     The broker keeps track of both registered clients and clients' subscriptions
477     in the clients registry.
478
479     In order to be advertised to clients during the subscription phase, tutors
480     should register to the broker using the \texttt{Register\_tutor} method of
481     the broker.  This method is really similar to \texttt{Register\_client}:
482     tutors are required to send an unique identifier and a base URI for their
483     \ws{}.
484     Additionally tutors are required to send an human readable description of
485     their capabilities; this information could be used by the client user to
486     decide which tutors she wants to subscribe to. As the clients, tutors can
487     unregister from brokers using \texttt{Unregister\_broker} method.
488
489     Each time the client status changes, it get sent sent to the
490     broker using its \texttt{Status} method. Using both the clients registry (to
491     lookup the client's subscription) and the tutors registry (to check if some tutors
492     have unsubscribed), the broker is able to decide to which tutors the
493     new status have to be forwarded.
494 %   \ednote{CSC: qui o nei lavori futuri parlare
495 %    della possibilit\'a di avere un vero brocker che multiplexi le richieste
496 %    dei client localizzando i servizi, etc.}
497
498     The forwarding operation is performed using the \texttt{Start\_musing}
499     method of the tutors, that is a request to start a new computation
500     (\emph{\musing{}}) on a given status. The return value of
501     \texttt{Start\_musing} is a
502     \musing{} identifier that is saved in the \musings{} registry along with
503     the identifier of the client that triggered the \musing{}.
504
505     As soon as a tutor completes an \musing{}, it informs the broker
506     using its \texttt{Musing\_completed} method; the broker can now remove the
507     \musing{} entry from the \musings{} registry and, depending on its outcome,
508     inform the client. In case of success one of the \texttt{Musing\_completed}
509     arguments is a hint to be sent to the client; otherwise there is no need to
510     inform him and the \texttt{Musing\_completed} method is called
511     just to update the \musings{} registry.
512
513     Consulting the \musings{} registry, the broker is able to know, at each
514     time, which \musings{} are in execution on which tutor. This peculiarity is
515     exploited by the broker on invocation of the \texttt{Status} method.
516     Receiving a new status from the client implies indeed that the previous
517     status no longer exists and all \musings{} working on it should be stopped:
518     additionally to the already described behavior (i.e. starting new
519     \musings{} on the received status), the broker takes also care of stopping
520     ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
521
522 %CASSATO
523 %   \paragraph{\wss{}}
524 %     As already discussed, all \hbugs{} actors act as \wss{} offering one or more
525 %     services to neighbor actors. To grant as most accessibility as possible to
526 %     our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given
527 %     that our proof assistant was entirely developed in the Objective Caml
528 %     language, we have chosen to develop also \hbugs{} in that language in order
529 %     to maximize code reuse. To develop \wss{} in Objective Caml we have
530 %     developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
531 %     write HTTP 1.1 Web servers and abstracts over GET/POST parsing. This library
532 %     supports different kinds of Web servers architectures, including
533 %     multi-process and multi-threaded ones.} bindings described in
534 %     \cite{wsdlbindings}.
535
536   \paragraph{Tutors}
537     Each tutor exposes a \ws{} interface and should be able to work, not only for
538     many different clients referring to a common broker, but also for many
539     different brokers. The potential high number of concurrent clients imposes
540     a multi-threaded or multi-process architecture.
541
542     Our current implementation is based on a multi threaded architecture
543     exploiting the capabilities of the O'HTTP library \cite{zack}. Each tutor is
544     composed by one always running thread plus an additional thread for each
545     \musing{}.
546     One thread is devoted to listening for incoming \ws{} requests; when a
547     request is received the control is passed to a second thread, created on the
548     fly, that handle the incoming request (usual one-thread-per-request approach
549     in web servers design).
550     In particular if the received request is \texttt{Start\_musing}, a new thread is
551     spawned to handle it; the thread in duty to handle the HTTP request
552     returns an HTTP response containing the identifier of the just started
553     \texttt{musing}, and then dies. If the received request is
554     \texttt{Stop\_musing}, instead, the spawned thread kills the thread
555     responsible for the \texttt{musing} whose identifier is the argument
556     of the \texttt{Stop\_musing} method.
557     
558     This architecture turns out to be scalable and allows the running threads
559     to share the cache of loaded (and type-checked) theorems.
560     As we will explain in Sect. \ref{tutors}, this feature turns out to be
561     really useful for tactics that rely on a huge but fixed set of lemmas,
562     as every reflexive tactic.
563
564     The implementation of a tutor within the described architecture is not that
565     difficult having a language with good threading capabilities (as OCaml has)
566     and a pool of already implemented tactics (as \texttt{gTopLevel} has).
567     Working with threads is known to be really error prone due to
568     concurrent programming intrinsic complexity. Moreover, there is a
569     non-neglectable part of code that needs to be duplicated in every tutor:
570     the code to register the tutor to the broker and to handle HTTP requests;
571     the code to manage the creation and termination of threads; and the code for
572     parsing the requests and serializing the answers. As a consequence we
573     have written a generic implementation of a tutor which is parameterized
574     over the code that actually proposes the hint and over some administrative
575     data (as the port the tutor will be listening to).
576
577     The generic tutor skeleton is really helpful in writing new tutors.
578     Nevertheless, the code obtained by converting existing tactics into tutors
579     is still quite repetitive: every tutor that wraps a tactic has to
580     instantiate its own copy of the proof-engine kernel and, for each request,
581     it has to override its status, guess the tactic arguments, apply the tactic
582     and, in case of success, send back a hint with the tactic name and the
583     chosen arguments. Of course, the complex part of the work is guessing the
584     right arguments. For the simple case of tactics that do not require
585     any argument, though, we are able to automatically generate the whole
586     tutor code given the tactic name. Concretely, we have written a
587     tactic-based tutor template and a script that parses an XML file with
588     the specification of the tutor and generates the tutor's code.
589     The XML file describes the tutor's port, the code to invoke the tactic,
590     the hint that is sent back upon successful application and a
591     human readable explanation of the tactic implemented by the tutor.
592
593 \section{The Implemented \hbugs Tutors}
594 \label{tutors}
595 To test the \hbugs{} architecture and to assess the utility of a suggestion
596 engine for the end user, we have implemented several tutors. In particular,
597 we have investigated three classes of tutors:
598 \begin{enumerate}
599  \item \emph{Tutors for beginners}. These are tutors that implement tactics
600    which are neither computationally expensive nor difficult to understand:
601    an expert user can always understand if the tactic can be applied or not
602    without having to try it. For example, the following implemented tutors
603    belong to this class:
604     \begin{itemize}
605      \item \emph{Assumption Tutor}: it ends the proof if the thesis is
606        equivalent\footnote{In our implementation, the equivalence relation
607        imposed by the logical framework is \emph{convertibility}. Two
608        expressions are convertible when they reduce to the same normal form.
609        Two ``equal'' terms depending on free variables can be non-convertible
610        since free variables stop the reduction. For example, $2x$ is convertible
611        with $(3-1)x$ because they both reduce to the same normal form
612        $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
613        already in normal form.}
614        to one of the hypotheses\footnote{
615        In some cases, especially when non-trivial computations are involved,
616        the user is totally unable to figure out the convertibility of two terms.
617        In these cases the tutor becomes handy also for expert users.}.
618      \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
619        adsurdum} if one hypothesis is equivalent to $False$.
620      \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
621        suggests to apply the commutative property.
622      \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
623        the Constructor Tutor suggests to proceed in the proof by applying one
624        or more constructors when the goal thesis is an inductive type or a
625        proposition inductively defined according to the declarative
626        style\footnote{An example of a proposition that can be given in
627        declarative style is the $\le$ relation over natural numbers:
628        $\le$ is the smallest relation
629        such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
630        that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
631        of $n \le n$ is simply the application of the first constructor to
632        $n$ and a proof of $n \le m$ is the application of the second
633        constructor to $n,m$ and a proof of $n \le m$.}.
634        Since disjunction, conjunction, existential quantification and
635        Leibniz equality are particular cases of inductive propositions,
636        all the other tutors of this class are instantiations of the
637        the Constructor tactic. Left and Right suggest to prove a disjunction
638        by proving its left/right member; Split reduces the proof of a
639        conjunction to the two proof of its members; Exists suggests to
640        prove an existential quantification by providing a
641        witness\footnote{This task is left to the user.}; Reflexivity proves
642        an equality whenever the two sides are convertible.
643     \end{itemize}
644   Beginners, when first faced with a tactic-based proof-assistant, get
645   lost quite soon since the set of tactics is large and their names and
646   semantics must be remembered by heart. Tutorials are provided to guide
647   the user step-by-step in a few proofs, suggesting the tactics that must
648   be used. We believe that our beginners tutors can provide an auxiliary
649   learning tool: after the tutorial, the user is not suddenly left alone
650   with the system, but she can experiment with variations of the exercises given
651   in the tutorial as much as she like, still getting useful suggestions.
652   Thus the user is allowed to focus on learning how to do a formal proof
653   instead of wasting efforts trying to remember the interface to the system.
654  \item \emph{Tutors for Computationally Expensive Tactics}. Several tactics have
655   an unpredictable behavior, in the sense that it is unfeasible to understand
656   whether they will succeed or they will fail when applied and what will be
657   their result. Among them, there are several tactics either computationally
658   expensive or resource consuming. In the first case, the user is not
659   willing to try a tactic and wait for a long time just to understand its
660   outcome: she would prefer to keep on concentrating on the proof and
661   have the tactic applied in background and receive out-of-band notification
662   of its success. The second case is similar, but the tactic application must
663   be performed on a remote machine to avoid overloading the user host
664   with several concurrent resource consuming applications.
665
666   Finally, several complex tactics and in particular all the tactics based
667   on reflexive techniques depend on a pretty large set of definitions, lemmas
668   and theorems. When these tactics are applied, the system needs to retrieve
669   and load all the lemmas. Pre-loading all the material needed by every
670   tactic can quickly lead to long initialization times and to large memory
671   footstamps. A specialized tutor running on a remote machine, instead,
672   can easily pre-load the required theorems.
673
674   As an example of computationally expensive task, we have implemented
675   a tutor for the \emph{Ring} tactic \cite{ringboutin}.
676   The tutor is able to prove an equality over a ring by reducing both members
677   to a common normal form. The reduction, which may require some time in
678   complex cases,
679   is based on the usual commutative, associative and neutral element properties
680   of a ring. The tactic is implemented using a reflexive technique, which
681   means that the reduction trace is not stored in the proof-object itself:
682   the type-checker is able to perform the reduction on-the-fly thanks to
683   the conversion rules of the system. As a consequence, in the library there
684   must be stored both the algorithm used for the reduction and the proof of
685   correctness of the algorithm, based on the ring axioms. This big proof
686   and all of its lemmas must be retrieved and loaded in order to apply the
687   tactic. The Ring tutor loads and caches all the required theorems the
688   first time it is contacted.
689  \item \emph{Intelligent Tutors}. Expert users can already benefit from the previous
690   class of tutors. Nevertheless, to achieve a significative production gain,
691   they need more intelligent tutors implementing domain-specific theorem
692   provers or able to perform complex computations. These tutors are not just
693   plain implementations of tactics or decision procedures, but can be
694   more complex software agents interacting with third-parties software,
695   such as proof-planners, CAS or theorem-provers.
696
697   To test the productivity impact of intelligent tutors, we have implemented
698   a tutor that is interfaced with the \helm{}
699   Search-Engine\footnote{\url{http://helm.cs.unibo.it/library.html}} and that
700   is able to look for every theorem in the distributed library that can
701   be applied to proceed in the proof. Even if the tutor deductive power
702   is extremely limited\footnote{We do not attempt to check if the new goals
703   obtained applying a lemma can be automatically proved or, even better,
704   automatically disproved to reject the lemma.}, it is not unusual for
705   the tutor to come up with precious hints that can save several minutes of
706   work that would be spent in proving again already proven results or
707   figuring out where the lemmas could have been stored in the library.
708 \end{enumerate}
709
710 \section{Conclusions and Future Work}
711 \label{conclusions}
712   In this paper we described a suggestion engine architecture for
713   proof-assistants: the client (a proof-assistant) sends the current proof
714   status to several distributed \wss{} (called tutors) that try to progress
715   in the proof and, in case of success, send back an appropriate hint
716   (a proof-plan) to the user. The user, that in the meantime was able to
717   reason and progress in the proof, is notified with the hints and can decide
718   to apply or ignore them. A broker is provided to decouple the clients and
719   the tutors and to allow the client to locate and invoke the available remote
720   services. The whole architecture is an instance of the MONET architecture
721   for Mathematical \wss{}. It constitutes a reimplementation of the core
722   features of the pioneering \OmegaAnts{} system in the new \wss{}
723   framework.
724
725   A running prototype has been implemented as part of the
726   \helm{} project \cite{helm}
727   and we already provide several tutors. Some of them are simple tutors that
728   try to apply one or more tactics of the \helm{} Proof-Engine, which is also
729   our client. We also have a much more complex tutor that is interfaced
730   with the \helm{} Search-Engine and looks for lemmas that can be directly
731   applied.
732
733   Future works comprise the implementation of new features and tutors, and
734   the embedding of the system in larger test cases. For instance, one
735   interesting case study would be interfacing a CAS as Maple to the
736   \hbugs{} broker, developing at the same time a tutor that implements the
737   Field tactic of Coq, which proves the equality of two expressions in an
738   abstract field by reducing both members to the same normal form. CASs can
739   produce several compact normal forms, which are particularly informative
740   to the user and that may suggest how to proceed in a proof. Unfortunately,
741   CASs do not
742   provide any certificate about the correctness of the simplification. On
743   the contrary, the Field tactic certifies the equality of two expressions,
744   but produces normal forms that are hardly a simplification of the original
745   formula. The benefits for the CAS would be obtained by using the Field tutor
746   to certify the CAS simplifications, proving that the Field normal form
747   of an expression is preserved by the simplification.
748   More advanced tutors could exploit the CAS to reduce the
749   goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
750   certify the simplification according to the skeptical approach.
751
752   We have many plans for further developing both the \hbugs{} architecture and
753   our prototype. Interesting results could be obtained
754   augmenting the informative content of each suggestion. We can for example
755   modify the broker so that also negative results are sent back to the client.
756   Those negative suggestions could be reflected in the user interface by
757   deactivating commands to narrow the choice of tactics available to the user.
758   This approach could be interesting especially for novice users, but requires
759   the client to increase their level of trust in the other actors.
760
761   We plan also to add some rating mechanism to the architecture. A first
762   improvement in this direction could be distinguishing between hints that, when
763   applied, are able to completely close one or more goals, and
764   tactics that progress in the proof by reducing one or more goals to new goals:
765   since the new goals can be false, the user can be forced later on to
766   backtrack.
767
768   Other heuristics and or measures could be added to rate
769   hints and show them to the user in a particular order: an interesting one
770   could be a measure that try to minimize the size of the generated proof,
771   privileging therefore non-overkilling solutions \cite{ring}.
772
773   We are also considering to follow the \OmegaAnts{} path adding
774   ``recursion'' to the system so that the proof status resulting from the
775   application of old hints are cached somewhere and could be used as a starting
776   point for new hint searches. The approach is interesting, but it represents
777   a big shift towards automatic theorem proving: thus we must consider if it is
778   worth the effort given the increasing availability of automation in proof
779   assistants tactics and the ongoing development of \wss{} based on
780   already existent and well developed theorem provers.
781
782   Even if not strictly part of the \hbugs{} architecture, the graphical user
783   interface (GUI) of our prototype needs a lot of improvement if we want
784   it to be really usable by novices. In particular, a critical issue
785   is avoiding continuous distractions for the user determined by the hints
786   that are asynchronously pushed to her.
787
788   Our \wss{} still lack a real integration in the MONET architecture,
789   since we do not provide the different ontologies to describe our problems,
790   solutions, queries, and services. In the short term, completing this task
791   could provide a significative feedback to the MONET consortium and would
792   enlarge the current set of available MONET actors on the Web. In the long
793   term, new more intelligent tutors could be developed on top of already
794   existent MONET \wss{}.
795
796   To conclude, \hbugs{} is a nice experiment meant to understand whether the
797   current \wss{} technology is mature enough to have a concrete and useful
798   impact on the daily work of proof-assistants users. So far, only the tutor
799   that is interfaced with the \helm{} Search-Engine has effectively increased
800   the productivity of experts users. The usefulness of the tutors developed for
801   beginners, instead, need further assessment.
802
803 \begin{thebibliography}{01}
804
805 \bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
806  \url{http://www.w3.org/TR/2003/WD-ws-gloss-20030514/}
807
808 \bibitem{wsdlbindings} Web Services Description Language (WSDL)
809  Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
810  \url{http://www.w3.org/TR/wsdl12-bindings/}
811
812 \bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
813  Deduction Systems via the Logic Broker Architecture. In Proceedings
814  of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
815
816 \bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
817  the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
818  Austria, May 2002.
819
820 \bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
821  Mathematical Knowledge Management in HELM. In Annals of Mathematics and
822  Artificial Intelligence, 38(1): 27--46, May 2003.
823
824 \bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
825  at Combining Interactive and Automated Theorem Proving. In M. Kerber and
826  M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
827  81--97, 2000.
828
829 \bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
830  Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
831  Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
832
833 \bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler,
834  X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier,
835  W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical
836  Assistant. In W. McCune (ed), Proceedings of the 14th Conference on
837  Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255,
838  Townsville, Australia, 1997.
839
840 \bibitem{ringboutin} S. Boutin. Using reflection to build efficient and
841  certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
842  TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
843
844 \bibitem{maplemodeforCoq} David Delahaye, Micaela Mayero.
845  A Maple Mode for Coq. Contribution to the Coq library.\\
846  \url{htpp://coq.inria.fr/contribs/MapleMode.html}
847
848 \bibitem{MONET-Overview} The MONET Consortium, MONET Architecture Overview,
849  Public Deliverable D04 of the MONET Project.\\
850  \url{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
851
852 \bibitem{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable
853  D2.a.\\
854  \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html}
855
856 \bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the
857  Bad Habit of Overkilling. In Supplementary Proceedings of the 14th
858  International Conference TPHOLS 2001, pp. 352--367, Edinburgh.
859
860 \bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
861  dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
862
863 \bibitem{ws3} J. Zimmer and M. Kohlhase. System Description: The MathWeb
864  Software Bus for Distributed Mathematical Reasoning.
865  In Proceedings of the 18th International Conference on Automated Deduction
866  CADE 18, LNAI 2392, Springer Verlag, 2002.
867
868 \bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
869  Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
870
871 \end{thebibliography}
872  
873 \end{document}