1 \documentclass[runningheads]{llncs}
7 % \myincludegraphics{filename}{place}{width}{caption}{label}
8 \newcommand{\myincludegraphics}[5]{
11 \includegraphics[width=#3]{eps/#1.eps}
19 \usepackage{draftstamp}
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}
30 \title{Brokers and Web-Services for Automatic Deduction: a Case Study}
32 \author{Claudio Sacerdoti Coen \and Stefano Zacchiroli}
35 Department of Computer Science\\
36 University of Bologna\\
37 Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
38 \email{sacerdot@cs.unibo.it}
40 Department of Computer Science\\
41 \'Ecole Normale Sup\'erieure\\
42 45, Rue d'Ulm, F-75230 Paris Cedex 05, FRANCE\\
43 \email{zack@cs.unibo.it}
53 We present a planning broker and several Web-Services for automatic deduction.
54 Each Web-Service implements one of the tactics usually available in
55 interactive proof-assistants. When the broker is submitted a "proof status" (an
56 incomplete proof tree and a focus on an open goal) it dispatches the proof to
57 the Web-Services, collects the successful results, and send them back to the
58 client as "hints" as soon as they are available.
60 In our experience this architecture turns out to be helpful both for
61 experienced users (who can take benefit of distributing heavy computations)
62 and beginners (who can learn from it).
65 \section{Introduction}
66 The \ws{} approach at software development seems to be a working solution for
67 getting rid of a wide range of incompatibilities between communicating
68 software applications. W3C's efforts in standardizing related technologies
69 grant longevity and implementations availability for frameworks based on
70 \wss{} for information exchange. As a direct consequence, the number of such
71 frameworks is increasing and the World Wide Web is moving from a disorganized
72 repository of human-understandable HTML documents to a disorganized repository
73 of applications working on machine-understandable XML documents both for input
76 The big challenge for the next future is to provide stable and reliable
77 services over this disorganized, unreliable and ever-evolving architecture.
78 The standard solution is to provide a further level of
79 stable services (called \emph{brokers}) that behave as common gateways/addresses
80 for client applications to access a wide variety of services and abstract over
83 Since the \emph{Declaration of Linz}, the MONET
84 Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}}
85 is working on the development of a framework, based on the
86 \wss{}/brokers approach, aimed at providing a set of software tools for the
87 advertisement and the discovery of mathematical \wss{}.
88 %CSC This framework turns out to be strongly based on both \wss{} and brokers.
90 Several groups have already developed software bus and
91 services\footnote{The most part of these systems predate the development of
92 \wss. Those systems whose development is still active are slowly being
93 reimplemented as \wss.} providing both computational and reasoning
94 capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of
95 Computer Algebra Systems; the second ones provide interfaces to well-known
97 Proof-planners, proof-assistants, CAS and
98 domain-specific problem solvers are natural candidates to be clients of these
99 services. Nevertheless, so far the number of examples in the literature has
100 been extremely low and the concrete benefits are still to be assessed.
102 In this paper we present an architecture, namely \hbugs{}, implementing a
103 \emph{suggestion engine} for the proof assistant developed on behalf of the
104 \helm{}\footnote{Hypertextual Electronic Library of Mathematics,
105 \url{http://helm.cs.unibo.it}} project
106 \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to
107 suggest possible ways to proceed in a proof. The tutors are orchestrated
108 by a broker (a \ws{} itself) that is able to dispatch a proof
109 status from a client (the proof-assistant) to the tutors;
110 each tutor try to make progress in the proof and, in case
111 of success, notify the client that shows an \emph{hint} to the user.
112 The broker is an instance of the homonymous entity of the MONET framework.
113 The tutors are MONET services. Another \ws{} (which is not described in this
114 paper and which is called Getter \cite{zack}) is used to locate and download
115 mathematical entities; the Getter plays the role of the Mathematical Object
116 Manager in the MONET framework.
118 A precursor of \hbugs{} is the \OmegaAnts{} project
119 \cite{omegaants1,omegaants2}, which provided similar functionalities to the
120 \Omegapp{} proof-planner \cite{omega}. The main architectural difference
121 between \hbugs{} and \OmegaAnts{} are that the latter is based on a
122 black-board architecture and it is not implemented using \wss{} and
125 In Sect. \ref{architecture} we present the architecture of \hbugs{}.
126 Further implementation details are given in Sect. \ref{implementation}.
127 Sect. \ref{tutors} is an overview of the tutors that have been implemented.
128 As usual, the final section of this paper is devoted to conclusions and future works.
130 \section{An \hbugs{} Bird's Eye View}
132 \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
134 The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
135 different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
136 Each actor present one or more \ws{} interfaces to its neighbors \hbugs{}
139 In this section we detail the role and requirements of each kind of
140 actors and discuss about the correspondences between them and the MONET
141 entities described in \cite{MONET-Overview}.
144 An \hbugs{} client is a software component able to produce \emph{proof
145 status} and to consume \emph{hints}.
147 A proof status is a representation of an incomplete proof and is supposed to
148 be informative enough to be used by an interactive proof assistant. No
149 additional requirements exist on the proof status, but there should be an
150 agreement on its format between clients and tutors. An hint is an
151 encoding of a step that can be performed in order to proceed in an
152 incomplete proof. Usually it represents a reference to a tactic available
153 on some proof assistant along with an instantiation for its formal
154 parameters. More structured hints can also be used: an hint can be
155 as complex as a whole proof-plan.
157 Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
158 providers and requesters, see Fig. \ref{interfaces}.
159 They act as providers for the broker (to receive hints)
160 and as requesters (to submit new status). Clients
161 additionally use broker service to know which tutors are available and to
162 subscribe to one or more of them.
164 Usually, when the client role is taken by an interactive proof assistant,
165 new status are sent to the broker as soon as the proof change (e.g. when the
166 user applies a tactic or when a new proof is started) and hints are shown to
167 the user be the means of some effect in the user interface (e.g. popping a
168 dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
169 possibile posto dove mettere una reference a una mini-sessione interattiva.
170 \'E l'appendice un posto dove metterla?}
172 \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
173 {\hbugs{} \wss{} interfaces}
175 \hbugs{} clients act as MONET clients and ask brokers to provide access to a
176 set of services (the tutors). \hbugs{} has no actors corresponding to
177 MONET's Broker Locating Service (since the client is supposed to know the
178 URI of at least one broker). The \hbugs{} client and tutors contact the
179 Getter (a MONET Mathematical Object Manager) to locate and retrieve
180 mathematical items in the \helm{} library.
181 The proof status that are exchanged
182 by the \hbugs{} actors, instead, are built on the fly and are neither
183 stored nor given an unique identifier (URI) to be managed by the
187 Brokers are the key actors of the \hbugs{} architecture since they
188 act as intermediaries between clients and tutors. They behave as \wss{}
189 providers and requesters for \emph{both} clients and tutors, see Fig.
192 With respect to the client, a broker acts as a \ws{} provider, receiving the
193 proof status and forwarding it to one or more tutors.
194 It also acts as a \ws{} requester sending
195 hints to the client as soon as they are available from the tutors.
197 With respect to the tutors, the \ws{} provider role is accomplished by
198 receiving hints as soon as they are produced; as a requester, it is
199 accomplished by asking for computations (\emph{musings} in \hbugs{}
200 terminology) on status received by clients and by stopping already late but
201 still ongoing \musings{}.
203 Additionally brokers keep track of available tutors and clients
206 \hbugs{} brokers act as MONET brokers implementing the following components:
207 Client Manager, Service Registry Manager (keeping track of available
208 tutors), Planning Manager (choosing the available tutors among the ones to
209 which the client is subscribed), Execution Manager. The Service Manager
210 component is not required since the session handler, that identifies
211 a session between a service and a broker, is provided to the service by
212 the broker instead of being received from the service when the session is
213 initialized. In particular, a session is identified by an unique identifier
214 for the client (its URL) and an unique identifier for the broker (its
217 The MONET architecture specification does not state explicitly whether
218 the service and broker answers can be asynchronous. Nevertheless, the
219 described information flow implicitly suggests a synchronous implementation.
220 On the contrary, in \hbugs{} every request is asynchronous: the connection
221 used by an actor to issue a query is immediately closed; when a service
222 produces an answer, it gives it back to the issuer by calling the
223 appropriate actor's method.
226 Tutors are software component able to consume proof status producing hints.
227 \hbugs{} does not specify by which means hints should be produced: tutors
228 can use any means necessary (heuristics, external theorem prover or CAS,
229 etc.). The only requirement is that there exists an agreement on the
230 formats of proof status and hints.
232 Tutors act both as \ws{} providers and requesters for the broker, see Fig.
234 providers, they wait for commands requesting to start a new \musing{} on
235 a given proof status or to stop an old, out of date, \musing{}. As
236 requesters, they signal to the broker the end of a \musing{} along with its
237 outcome (an hint in case of success or a failure notification).
239 \hbugs{} tutors act as MONET services.
241 \section{An \hbugs{} Session Example}
243 \section{Implementation's Highlights}
244 \label{implementation}
245 In this section we present some of the most relevant implementation details of
246 the \hbugs{} architecture.
249 \paragraph{Proof status}
250 In our implementation of the \hbugs{} architecture we used the proof
251 assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
252 client. Thus we have implemented serialization/deserialization capabilities
253 for its internal status. In order to be able to describe \wss{} that
254 exchange status in WSDL using the XML Schema type system, we have chosen an
255 XML format as the target format for the serialization.
257 A schematic representation of the gTopLevel internal status is depicted in
258 Fig. \ref{status}. Each proof is represented by a tuple of four elements:
259 \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
261 \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
265 \item[uri]: an URI chosen by the user at the beginning of the proof
266 process. Once (and if) proved, that URI will globally identify the term
267 inside the \helm{} library (given that the user decides to save it).
268 \item[thesis]: the thesis of the ongoing proof
269 \item[proof]: the current incomplete proof tree. It can contain
270 \emph{metavariables} (holes) that stands for the parts of the proof
271 that are still to be completed. Each metavariable appearing in the
272 tree references one element of the metavariables environment
274 \item[metasenv]: the metavariables environment is a list of
275 \emph{goals} (unproved conjectures).
276 In order to complete the proof, the user has to instantiate every
277 metavariable in the proof with a proof of the corresponding goal.
278 Each goal is identified by an unique identifier and has a context
279 and a type (the goal thesis). The context is a list of named
280 hypotheses (declarations and definitions). Thus the context and the goal
281 thesis form a sequent, which is the statement of the proof that will
282 be used to instantiate the metavariable occurrences.
285 Each of these information is represented in XML as described in
286 \cite{mowglicic}. Additionally, an \hbugs{} status carry the unique
287 identifier of the current goal, which is the goal the user is currently
288 focused on. Using this value it is possible to implement different client
289 side strategies: the user could ask the tutors to work on the goal
290 she is considering or to work on the other ``background'' goals.
293 An hint in the \hbugs{} architecture should carry enough information to
294 permit the client to progress in the current proof. In our
295 implementation each hint corresponds to either one of the tactics available
296 to the user in gTopLevel (together with its actual arguments) or a set
297 of alternative suggestions (a list of hints).
299 For tactics that don't require any particular argument (like tactics that
300 apply type constructors or decision procedures)
301 only the tactic name is represented in the hint. For tactics that need
302 terms as arguments (for example the \texttt{Apply} tactic that apply a
303 given lemma) the hint includes a textual representation of them, using the
304 same representation used by the interactive proof assistant when querying
305 user for terms. In order to be transmitted between \wss{}, hints are
308 It is also possible for a tutor to return more hints at once,
309 grouping them in a particular XML element.
310 This feature turns out to be particularly useful for the
311 \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that
312 query a lemma database and return to the client a list of all lemmas that
313 could be used to complete the proof. This particular hint is encoded as a
314 list of \texttt{Apply} hints, each of them having one of the results as term
317 We would like to stress that the \hbugs{} architecture has no dependency
318 on either the hint or the status representation: the only message parts
319 that are fixed are those representing the administrative messages
320 (the envelops in the \wss{} terminology). In particular, the broker can
321 manage at the same time several sessions working on different status/hints
322 formats. Of course, there must be an agreement between the clients
323 and the tutors on the format of the data exchanged.
325 In our implementation the client does not trust the tutors hints:
326 being encoded as references to available tactics imply
327 that an \hbugs{} client, on receipt of an hint, simply try to reply the work
328 done by a tutor on the local copy of the proof. The application of the hint
329 can even fail to type check and the client copy of the proof can be left
330 undamaged after spotting the error. Note, however, that it is still
331 possible to implement a complex tutor that looks for a proof doing
333 send back to the client an hint whose argument is a witness (a trace) of
334 the proof found: the client applies the hint reconstructing (and checking
335 the correctness of) the proof from the witness, without having to
336 re-discover the proof itself.
337 \ednote{Zack: che ne dici di un "reinvent the whell" qui sopra? fa sempre
340 An alternative implementation where the tutors are trusted would simply
341 send back to the client a new proof-status. Upon receiving the
342 proof-status, the client would just override its current proof status with
343 the suggested one. In the case of those clients which are implemented
344 using proof-objects (as the Coq proof-assistant, for instance), it is
345 still possible for the client to type-check the proof-object and reject
346 wrong hints. The systems that are not based on proof-objects
347 (as PVS, NuPRL, etc.), instead, have to trust the new proof-status. In this
348 case the \hbugs{} architecture needs at least to be extended with
349 clients-tutors authentication.
351 \paragraph{Registries}
352 Being central in the \hbugs{} architecture, the broker is also responsible
353 of housekeeping operations both for clients and tutors. These operations are
354 implemented using three different data structures called \emph{registries}:
355 clients registry, tutors registry and \musings{} registry.
357 In order to use the suggestion engine a client should register itself to the
358 broker and subscribe to one or more tutors. The registration phase is
359 triggered by the client using the \texttt{Register\_client} method of the
360 broker to send him an unique identifier and its base URI as a
361 \ws{}. After the registration, the client can use broker's
362 \texttt{List\_tutors} method to get a list of available tutors.
363 Eventually the client can subscribe to one or more of these using broker's
364 \texttt{Subscribe} method. Clients can also unregister from brokers using
365 \texttt{Unregister\_client} method.
367 The broker keeps track of both registered clients and clients' subscriptions
368 in the clients registry.
370 In order to be advertised to clients during the subscription phase, tutors
371 should register to the broker using the broker's \texttt{Register\_tutor}
372 method. This method is really similar to \texttt{Register\_client}:
373 tutors are required to send an unique identify and a base URI for their
375 Additionally tutors are required to send an human readable description of
376 their capabilities; this information could be used by client's user to
377 decide which tutors he needs to subscribe to. Like clients\ednote{Zack: mi
378 pare che questo sia un caso in cui si debba usare "as" e non like, ma non ne
379 sono certo}, tutors can
380 unregister from brokers using \texttt{Unregister\_broker} method.
382 Each time the client status change, it get sent sent to the
383 broker using its \texttt{Status} method. Using both clients registry (to
384 lookup client's subscription) and tutors registry (to check if some tutors
385 has unsubscribed), the broker is able to decide to which tutors the
386 new status have to be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
387 della possibilit\'a di avere un vero brocker che multiplexi le richieste
388 dei client localizzando i servizi, etc.}
390 The forwarding operation is performed using the \texttt{Start\_musing}
391 method of the tutors, that is a request to start a new computation
392 (\emph{\musing{}}) on a given status. The return value of
393 \texttt{Start\_musing} is a
394 \musing{} identifier that is saved in the \musings{} registry along with
395 the identifier of the client that triggered the \musing{}.
397 As soon as a tutor completes an \musing{}, it informs the broker
398 using its \texttt{Musing\_completed} method; the broker can now remove the
399 \musing{} entry from the \musings{} registry and, depending on its outcome,
400 inform the client. In case of success one of the \texttt{Musing\_completed}
401 arguments is an hint to be sent to the client, otherwise there's no need to
402 inform him and the \texttt{Musing\_completed} method is called
403 just to update the \musings{} registry.
405 Consulting the \musings{} registry, the broker is able to know, at each
406 time, which \musings{} are in execution on which tutor. This peculiarity is
407 exploited by the broker on invocation of the \texttt{Status} method.
408 Receiving a new status from the client implies indeed that the previous
409 status no longer exists and all \musings{} working on it should be stopped:
410 additionally to the already described behavior (i.e. starting new
411 \musings{} on the received status), the broker takes also care of stopping
412 ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
415 As already discussed, all \hbugs{} actors act as \wss{} offering one or more
416 services to neighbor actors. To grant as most accessibility as possible to
417 our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given
418 that our proof assistant was entirely developed in the Objective Caml
419 language, we have chosen to develop also \hbugs{} in that language in order
420 to maximize code reuse. To develop \wss{} in Objective Caml we have
421 developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
422 write HTTP 1.1 Web servers and abstract over GET/POST parsing. This library
423 supports different kinds of Web servers architecture, including
424 multi-process and multi-threaded ones.} bindings described in
428 Each tutor expose a \ws{} interface and should be able to work, not only for
429 many different clients referring to a common broker, but also for many
430 different brokers. The potential high number of concurrent clients imposes
431 a multi-threaded or multi-process architecture.
433 Our current implementation is based on a multi threaded architecture
434 exploiting the capabilities of the O'HTTP library. Each tutor is composed
435 by one thread always running plus
436 an additional thread for each running \musing{}. One thread is devoted to
437 listening for incoming \ws{} request; upon correct receiving requests it
438 pass the control to a second thread, created on the fly, to handle the
439 incoming request following the classical one-thread-per-request approach in
441 If the received request is \texttt{Start\_musing}, a new thread is
442 spawned to handle it; the thread in duty to handle the HTTP request
443 returns an HTTP response containing the identifier of the just started
444 \texttt{musing}, and then dyes. If the received request is
445 \texttt{Stop\_musing}, instead, the spawned thread kills the thread
446 responsible for the \texttt{musing} whose identifier is the argument
447 of the \texttt{Stop\_musing} method.
449 This architecture turns out to be scalable and allows the running threads
450 to share the cache of loaded (and type-checked) theorems.
451 As we will explain in Sect. \ref{tutors}, this feature turns out to be
452 really useful for tactics that rely on a huge but fixed set of lemmas,
453 as every reflexive tactic.
455 The implementation of a tutor with the described architecture is not that
456 difficult having a language with good threading capabilities (as OCaml has)
457 and a pool of already implemented tactics (as gTopLevel has).
458 Still working with threads is known to be really error prone due to
459 concurrent programming intrinsic complexity. Moreover, there is a
460 non-neglectable part of code that needs to be duplicated in every tutor:
461 the code to register the tutor to the broker and to handle HTTP requests;
462 the code to manage the creation and termination of threads; and the code for
463 parsing the requests and serializing the answers. As a consequence we
464 have written a generic implementation of a tutor which is parameterized
465 over the code that actually propose the hint and some administrative
466 data (as the port the tutor will be listening to).
468 The generic tutor skeleton is really helpful in writing new tutors.
469 Nevertheless, the code obtained by converting existing tactics into tutors
470 is still quite repetitive: every tutor that wraps a tactic has to
471 instantiate its own copy of the proof-engine kernel and, for each request,
472 it has to override its status, guess the tactic arguments, apply the tactic
473 and, in case of success, send back an hint with the tactic name and the
474 chosen arguments. Of course, the complex part of the work is guessing the
475 right arguments. For the simple case of tactics that do not require
476 any argument, though, we are able to automatically generate the whole
477 tutor code given the tactic name. Concretely, we have written a
478 tactic-based tutor template and a script that parses an XML file with
479 the specification of the tutor and generates the tutor's code.
480 The XML file describes the tutor's port, the code to invoke the tactic,
481 the hint that is sent back upon successful application and a
482 human readable explanation of the tactic implemented by the tutor.
484 \section{The Implemented \hbugs Tutors}
486 To test the \hbugs{} architecture and to assess the utility of a suggestion
487 engine for the end user, we have implemented several tutors. In particular,
488 we have investigated three classes of tutors:
490 \item \emph{Tutors for beginners}. These are tutors that implement tactics
491 which are neither computationally expensive nor difficult to understand:
492 an expert user can always understand if the tactic can be applied or not
493 without having to try it. For example, the following implemented tutors
494 belong to this class:
496 \item \emph{Assumption Tutor}: it ends the proof if the thesis is
497 equivalent\footnote{In our implementation, the equivalence relation
498 imposed by the logical framework is \emph{convertibility}. Two
499 expressions are convertible when they reduce to the same normal form.
500 Two ``equal'' terms depending on free variables can be non-convertible
501 since free variables stop the reduction. For example, $2x$ is convertible
502 with $(3-1)x$ because they both reduce to the same normal form
503 $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
504 already in normal form.}
505 to one of the hypotheses\footnote{
506 In some cases, especially when non-trivial computations are involved,
507 the user is totally unable to figure out the convertibility of two terms.
508 In these cases the tutor becomes handy also for expert users.}.
509 \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
510 adsurdum} if one hypothesis is equivalent to $False$.
511 \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
512 suggests to apply the commutative property.
513 \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
514 the Constructor Tutor suggests to proceed in the proof by applying one
515 or more constructors when the goal thesis is an inductive type or a
516 proposition inductively defined according to the declarative
517 style\footnote{An example of a proposition that can be given in
518 declarative style is the $\le$ relation: $\le$ is the smallest relation
519 such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
520 that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
521 of $n \le n$ is simply the application of the first constructor to
522 $n$ and a proof of $n \le m$ is the application of the second
523 constructor to $n,m$ and a proof of $n \le m$.}.
524 \ednote{Zack: non e' necessario specificare che stai parlando di numeri
525 naturali nella footnote?}
526 Since disjunction, conjunction, existential quantification and
527 Leibniz equality are particular cases of inductive propositions,
528 all the other tutors of this class are instantiations of the
529 the Constructor tactic. Left and Right suggest to prove a disjunction
530 by proving its left/right member; Split reduces the proof of a
531 conjunction to the two proof of its members; Exists suggests to
532 prove an existential quantification by providing a
533 witness\footnote{This task is left to the user.}; Reflexivity proves
534 an equality whenever the two sides are convertible.
536 Beginners, when first faced with a tactic-based proof-assistant, get
537 lost quite soon since the set of tactics is large and their names and
538 semantics must be remembered by heart. Tutorials are provided to guide
539 the user step-by-step in a few proofs, suggesting the tactics that must
540 be used. We believe that our beginners tutors can provide an auxiliary
541 learning tool: after the tutorial, the user is not suddenly left alone
542 with the system, but she can experiment with variations of the proof given
543 in the tutorial as much as she like, still getting useful suggestions.
544 Thus the user is allowed to focus on learning how to do a formal proof
545 instead of wasting efforts trying to remember the interface to the system.
546 \item{Tutors for Computationally Expensive Tactics}. Several tactics have
547 an unpredictable behavior, in the sense that it is unfeasible to understand
548 whether they will succeed or they will fail when applied and what will be
549 their result. Among them, there are several tactics either computationally
550 expensive or resources consuming. In the first case, the user is not
551 willing to try a tactic and wait for a long time just to understand its
552 outcome: she would prefer to keep on concentrating on the proof and
553 have the tactic applied in background and receive out-of-band notification
554 of its success. The second case is similar, but the tactic application must
555 be performed on a remote machine to avoid overloading the user host
556 with several concurrent resource consuming applications.
558 Finally, several complex tactics and in particular all the tactics based
559 on reflexive techniques depend on a pretty large set of definitions, lemmas
560 and theorems. When these tactics are applied, the system needs to retrieve
561 and load all the lemmas. Pre-loading all the material needed by every
562 tactic can quickly lead to long initialization times and to large memory
563 footstamps. A specialized tutor running on a remote machine, instead,
564 can easily pre-load the required theorems.
566 As an example of computationally expensive task, we have implemented
567 a tutor for the \emph{Ring} tactic \cite{ringboutin}.
568 The tutor is able to prove an equality over a ring by reducing both members
569 to a common normal form. The reduction, which may require some time in
571 is based on the usual commutative, associative and neutral element properties
572 of a ring. The tactic is implemented using a reflexive technique, which
573 means that the reduction trace is not stored in the proof-object itself:
574 the type-checker is able to perform the reduction on-the-fly thanks to
575 the conversion rules of the system. As a consequence, in the library there
576 must be stored both the algorithm used for the reduction and the proof of
577 correctness of the algorithm, based on the ring axioms. This big proof
578 and all of its lemmas must be retrieved and loaded in order to apply the
579 tactic. The Ring tutor loads and cache all the required theorems the
580 first time it is contacted.
581 \item{Intelligent Tutors}. Expert users can already benefit from the previous
582 class of tutors. Nevertheless, to achieve a significative production gain,
583 they need more intelligent tutors implementing domain-specific theorem
584 provers or able to perform complex computations. These tutors are not just
585 plain implementations of tactics or decision procedures, but can be
586 more complex software agents interacting with third-parties software,
587 such as proof-planners, CAS or theorem-provers.
589 To test the productivity impact of intelligent tutors, we have implemented
590 a tutor that is interfaced with the \helm{}
591 Search-Engine\footnote{\url{http://helm.cs.unibo.it/library.html}} and that
592 is able to look for every theorem in the distributed library that can
593 be applied to proceed in the proof. Even if the tutor deductive power
594 is extremely limited\footnote{We do not attempt to check if the new goals
595 obtained applying a lemma can be automatically proved or, even better,
596 automatically disproved to reject the lemma.}, it is not unusual for
597 the tutor to come up with precious hints that can save several minutes of
598 work that would be spent in proving again already proven results or
599 figuring out where the lemmas could have been stored in the library.
602 \section{Conclusions and Future Work}
604 In this paper we described a suggestion engine architecture for
605 proof-assistants: the client (a proof-assistant) sends the current proof
606 status to several distributed \wss{} (called tutors) that try to progress
607 in the proof and, in case of success, send back an appropriate hint
608 (a proof-plan) to the user. The user, that in the meantime was able to
609 reason and progress in the proof, is notified with the hints and can decide
610 to apply or ignore them. A broker is provided to decouple the clients and
611 the tutors and to allow the client to locate and invoke the available remote
612 services. The whole architecture is an instance of the MONET architecture
613 for Mathematical \wss{}.
615 A running prototype has been implemented as part of the
616 \helm{} project \cite{helm}
617 and we already provide several tutors. Some of them are simple tutors that
618 try to apply one or more tactics of the \helm{} Proof-Engine, which is also
619 our client. We also have a much more complex tutor that is interfaced
620 with the \helm{} Search-Engine and looks for lemmas that can be directly
623 We have many plans for further developing both the \hbugs{} architecture and
624 our prototype. Interesting results could be obtained
625 augmenting the informative content of each suggestion. We can for example
626 modify the broker so that also negative results are sent back to the client.
627 Those negative suggestions could be reflected in the user interface by
628 deactivating commands to narrow the choice of tactics available to the user.
629 This approach could be interesting especially for novice users, but require
630 the client to trust other actors a bit more than in the current approach.
632 We plan also to add some rating mechanism to the architecture. A first
633 improvement in this direction could be distinguishing between hints that, when
634 applied, are able to completely close one or more goals and
635 tactics that progress in the proof by reducing one or more goals to new goals:
636 the new goals could be false and the proof can be closed only by backtracking.
638 Other heuristics and/or measures could be added to rate
639 hints and show them to the user in a particular order: an interesting one
640 could be a measure that try to minimize the size of the generated proof,
641 privileging therefore non-overkilling solutions \cite{ring}.
643 We are also considering to follow the \OmegaAnts{} path more closely adding
644 ``recursion'' to the system so that the proof status resulting from the
645 application of old hints are cached somewhere and could be used as a starting
646 point for new hint searches. The approach is interesting, but it represents
647 a big shift towards automatic theorem proving: thus we must consider if it is
648 worth the effort given the increasing availability of automation in proof
649 assistants tactics and the ongoing development of \wss{} based on
650 already existent and well developed theorem provers.
652 Even if not strictly part of the \hbugs{} architecture, the graphical user
653 interface (GUI) of our prototype needs a lot of improvement if we would like
654 it to be really usable by novices. In particular, the user is too easily
655 distracted by the tutor's hints that are ``pushed'' to her.
657 Our \wss{} still lack a real integration in the MONET architecture,
658 since we do not provide the different ontologies to describe our problems,
659 solutions, queries and services. In the short term, completing this task
660 could provide a significative feedback to the MONET consortium and would
661 enlarge the current set of available MONET actors on the Web. In the long
662 term, new more intelligent tutors could be developed on top of already
663 existent MONET \wss{}.
665 To conclude, \hbugs{} is a nice experiment meant to understand whether the
666 current \wss{} technology is mature enough to have a concrete and useful
667 impact on the daily work of proof-assistants users. So far, only the tutor
668 that is interfaced with the \helm{} Search-Engine has effectively increased
669 the productivity of experts users. The usefulness of the tutors developed for
670 beginners, instead, need further assessment.
672 \begin{thebibliography}{01}
674 \bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
675 \url{http://www.w3.org/TR/ws-gloss/}
677 \bibitem{wsdlbindings} Web Services Description Language (WSDL)
678 Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
679 \url{http://www.w3.org/TR/wsdl12-bindings/}
681 \bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
682 Deduction Systems via the Logic Broker Architecture. In Proceedings
683 of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
685 \bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
686 the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
689 \bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
690 Mathematical Knowledge Management in HELM. In Annals of Mathematics and
691 Artificial Intelligence, 38(1): 27--46, May 2003.
693 \bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
694 at Combining Interactive and Automated Theorem Proving. In M. Kerber and
695 M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
698 \bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
699 Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
700 Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
702 \bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler,
703 X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier,
704 W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical
705 Assistant. In W. McCune (ed), Proceedings of the 14th Conference on
706 Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255,
707 Townsville, Australia, 1997.
709 \bibitem{ringboutin} S. Boutin. Using reflection to build efficient and
710 certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
711 TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
713 \bibitem{MONET-Overview} The MONET Consortium, MONET Architecture Overview,
714 Public Deliverable D04 of the MONET Project.\\
715 \url{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
717 \bibitem{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable
719 \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html}
721 \bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the
722 Bad Habit of Overkilling. In Supplementary Proceedings of the 14th
723 International Conference TPHOLS 2001, pp. 352--367, Edinburgh.
725 \bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
726 dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
728 \bibitem{ws3} J. Zimmer and L. Dennis. Inductive Theorem Proving and
729 Computer Algebra in the MathWeb Software Bus. In Proceedings of the 10th
730 CALCULEMUS Symposium 2002, 3--5 July 2002.
732 \bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
733 Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
735 \end{thebibliography}