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 an
55 interactive proof-assistant. When the broker is submitted a "proof status" (an
56 unfinished proof tree and a focus on an open goal) it dispatches the proof to
57 the Web-Services, collects the successfull 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 conseguence, 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 \ednote{zack: buhm! :-P} is providing a further level of
79 stable services (called \emph{brokers}) that behave as common gateway/address
80 for client applications to access a wide variety of services and abstract over
83 Since the \emph{Declaration of Linz}, the MONET Consortium
84 \cite{MONET}, is working on the development of a framework, based on the
85 \wss{}/brokers approach, aimed at providing a set of software tools for the
86 advertisement and the discovery of mathematical \wss{}.
87 %CSC This framework turns out to be strongly based on both \wss{} and brokers.
89 Several groups have already developed \wss{} providing both computational and
90 reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
91 dalle conferenze calculemus}: the formers are implemented on top of
92 Computer Algebra Systems; the latters provide interfaces to well-known
93 theorem provers. Proof-planners, proof-assistants, CAS and
94 domain-specific problem solvers are natural candidates to be client of these
95 services. Nevertheless, so far the number of examples in the literature has
96 been extremely low and the concrete benefits are still to be assessed.
98 In this paper we present an architecture, namely \hbugs{}, implementing a
99 \emph{suggestion engine} for the proof assistant developed on behalf of the
100 \helm{}\footnote{Hypertextual Electronic Library of Mathematics,
101 \url{http://helm.cs.unibo.it}} project
102 \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to
103 suggest possible ways to proceed in a proof. The tutors are orchestrated
104 by a broker (a \ws{} itself) that is able to dispatch a proof
105 status from a client (the proof-assistant) to the tutors;
106 each tutor try to make progress in the proof and, in case
107 of success, notify the client that shows an \emph{hint} to the user.
108 The broker is an instance of the homonymous entity of the MONET framework.
109 The tutors are MONET services. Another \ws (which is not described in this
110 paper and which is called Getter \cite{}) is used to locate and download
111 mathematical entities; the Getter plays the role of the Mathematical Object
112 Manager in the MONET framework.
114 A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
115 which provided similar functionalities to the
116 \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
117 between \hbugs{} and \OmegaAnts{} are that the latter is based on a
118 black-board architecture and it is not implemented using \wss{} and
119 brokers. Other differences will be detailed in Sect. \ref{conclusions}
120 \ednote{CSC: che si fa di sta frase?}.
122 In Sect. \ref{architecture} we present the architecture of \hbugs{}.
123 Further implementation details are given in Sect. \ref{implementation}.
124 Sect. \ref{tutors} is an overview of the tutors that have been implemented.
125 As usual, the paper ends with the conclusions and future works.
128 {CSC: Non so se/dove mettere queste parti.
129 Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
130 non e' molto utile, ma la seconda sugli usi tipici di proof assistant
133 Despite of that the proof assistant case seems to be well suited to
134 investigate the usage of many different mathematical \wss{}. Indeed: most
135 proof assistants are still based on non-client/server architectures, are
136 application-centric instead of document-centric, offer a scarce level of
137 automation leaving entirely to the user the choice of which macro (usually
138 called \emph{tactic}) to use in order to make progress in a proof.
140 The average proof assistant can be, for example, a client of a \ws{}\
141 interfacing a specific or generic purpose theorem prover, or a client of a
142 \ws{} interfacing a CAS to simplify expressions in a particular mathematical
146 \section{An \hbugs{} Bird'S Eye View}
148 \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
150 The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
151 different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
152 Each actor present one or more \ws{} interfaces to its neighbours \hbugs{}
155 In this section we will detail the role and requirements of each kind of
156 actors and discuss about the correspondencies between them and the MONET
157 entities described in \cite{MONET-Overview}.
160 An \hbugs{} client is a software component able to produce \emph{proof
161 status} and to consume \emph{hints}.
163 A proof status is a representation of an incomplete proof and is supposed to
164 be informative enough to be used by an interactive proof assistant. No
165 additional requirements exist on the proof status, but there should be an
166 agreement on its format between clients and tutors. An hint is a
167 representation\ednote{CSC: non c'\'e un sinonimo pi\'u carino? Zack: l'unico
168 decente sembra essere nuovamente "suggestion". CSC: chiamalo sinonimo!}
169 of a step that can be performed in order to proceed in an
170 incomplete proof. Usually it represents a reference to a tactic available
171 on some proof assistant along with an instantiation for its formal
172 parameters. More structured hints can also be used: an hint can be
173 as complex as a whole proof-plan.
175 \myincludegraphics{interfaces}{t}{10cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
178 Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
179 providers and requesters, see Fig. \ref{interfaces}.
180 They act as providers for the broker (to receive hints)
181 and as requesters (to submit new status). Clients
182 additionally use broker service to know which tutors are available and to
183 subscribe to one or more of them.
185 Usually, when the role of client is taken by an interactive proof assistant,
186 new status are sent to the broker as soon as the proof change (e.g. when the
187 user applies a tactic or when a new proof is started) and hints are shown to
188 the user be the means of some effect in the user interface (e.g. popping a
189 dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
190 possibile posto dove mettere una mini-sessione interattiva. L'appendice
193 \hbugs{} clients act as MONET clients and ask brokers to provide access to a
194 set of services (the tutors). \hbugs{} has no actors corresponding to
195 MONET's Broker Locating Service (since the client is supposed to know the
196 URI of at least one broker). The \hbugs{} client and tutors contact the
197 Getter (a MONET Mathematical Object Manager) to locate and retrieve
198 mathematical items in the \helm{} library.
199 The proof status that are exchanged
200 by the \hbugs{} actors, instead, are built on the fly and are neither
201 stored nor are given an unique identifier (URI) to be managed by the
205 Brokers are the key actors of the \hbugs{} architecture since they
206 act as intermediaries between clients and tutors. They behave as \wss{}
207 providers and requesters for \emph{both} clients and tutors, see Fig.
210 With respect to client, a broker act as \ws{} provider, receiving the
211 proof status and forwarding it to one or more tutors.
212 It also acts as a \ws{} requester sending
213 hints to the client as soon as they are available from the tutors.
215 With respect to tutors, the \ws{} provider role is accomplished by receiving
216 hints as soon as they are produced; as a requester, it is accomplished
217 by asking for computations (\emph{musings} in \hbugs{} terminology) on
218 status received by clients and by stopping already late but still
220 \ednote{Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo
221 commento sulla utilita'/quantita' delle figure ... CSC: vanno benissimo}
223 Additionally brokers keep track of available tutors and clients
226 \hbugs{} brokers act as MONET brokers implementing the following components:
227 Client Manager, Service Registry Manager (keeping track of available
228 tutors), Planning Manager (chosing the available tutors among the ones to
229 which the client is subscribed), Execution Manager. The Service Manager
230 component is not required since the session handler, that identifies
231 a session between a service and a broker, is provided to the service by
232 the broker instead of being received from the service when it is
233 initialized. In particular, a session is identified by an unique identifier
234 for the client (its URL) and an unique identifier for the broker (its
235 URL).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i
236 multi-sessione. Ma mi sembra la strada che prenderemmo, no?}
238 The MONET architecture specification does not state explicitely whether
239 the service and broker answers can be asyncronous. Nevertheless, the
240 described information flow implicitly suggests a syncronous implementation.
241 On the contrary, in \hbugs{} every request is asyncronous: the connection
242 used by an actor to issue a query is immediately closed; when a service
243 produces an answer, it gives it back to the issuer by calling the
244 appropriate actor's method.
247 Tutors are software component able to consume proof status producing hints.
248 \hbugs{} doesn't specify by which means hints should be produced: tutors can
249 use any means necessary (heuristics, external theorem prover or CAS, ...).
250 The only requirement is that there exists an agreement on the formats of
251 proof status and hints.
253 Tutors act both as \ws{} providers and requesters for the broker. As
254 providers, they wait for commands requesting to start a new \musing{} on
255 a given proof status or to stop an old, out of date, \musing{}. As
256 requesters, they signal to the broker the end of a \musing{} along with its
257 outcome (an hint in case of success or a notification of failure).
259 \hbugs{} tutors act as MONET services.
261 \section{Implementation's Highlights}
262 \label{implementation}
263 In this section we present some of the most relevant implementation details of
264 the \hbugs{} architecture.
267 \paragraph{Proof status}
268 In our implementation of the \hbugs{} architecture we used the proof
269 assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
270 client. Thus we have implemented serialization/deserialization capabilities
271 for its internal status. In order to be able to describe \wss{} that
272 exchange status in WSDL using the XML Schema type system, we have chosen an
273 XML format as the target format for the serialization.
275 A schematic representation of the gTopLevel internal status is depicted in
276 Fig. \ref{status}. Each proof is representated by a tuple of four elements:
277 \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
279 \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
283 \item[uri]: an URI chosen by the user at the beginning of the proof
284 process. Once (and if) proved, that URI will globally identify the term
285 inside the \helm{} library (given that the user decides to save it).
286 \item[thesis]: the thesis of the ongoing proof
287 \item[proof]: the current incomplete proof tree. It can contain
288 \emph{metavariables} (holes) that stands for the parts of the proof
289 that are still to be completed. Each metavariable appearing in the
290 tree references one element of the metavariables environment
292 \item[metasenv]: the metavariables environment is a list of
293 \emph{goals} (unproved conjectures).
294 In order to complete the proof, the user has to instantiate every
295 metavariable in the proof with a proof of the corresponding goal.
296 Each goal is identified by an unique identifier and has a context
297 and a type ( the goal thesis). The context is a list of named
298 hypotheses (declarations and definitions). Thus the context and the goal
299 thesis form a sequent, which is the statement of the proof that will
300 be used to instatiate the metavariable occurrences.
303 Each of these information is represented in XML as described in
304 \cite{csc-thesis}. Additionally, an \hbugs{} status carry the unique
305 identifier of the current goal, which is the goal the user is currently
306 focused on. Using this value it is possible to implement different client
307 side strategies: the user could ask the tutors to work on the goal
308 she is considering or to work on the other ``background'' goals.
311 An hint in the \hbugs{} architecture should carry enough information to
312 permit the client to progress in the current proof. In our
313 implementation each hint corresponds to either one of the tactics available
314 to the user in gTopLevel (together with its actual arguments) or a set
315 of alternative suggestions (a list of hints).
317 For tactics that don't require any particular argument (like tactics that
318 apply type constructors or decision procedures)
319 only the tactic name is represented in the hint. For tactics that need
320 terms as arguments (for example the \texttt{Apply} tactic that apply a
321 given lemma) the hint includes a textual representation of them, using the
322 same representation used by the interactive proof assistant when querying
323 user for terms. In order to be trasmitted between \wss{}, hints are
326 It is also possible for a tutor to return more hints at once,
327 grouping them in a particular XML element.
328 This feature turns out to be particulary useful for the
329 \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that
330 query a lemma database and return to the client a list of all lemmas that
331 could be used to complete the proof. This particular hint is encoded as a
332 list of \texttt{Apply} hints, each of them having one of the results as term
335 We would like to stress that the \hbugs{} architecture has no dependency
336 on either the hint or the status representation: the only message parts
337 that are fixed are those representing the administrative messages
338 (the envelops in the \wss{} terminology). In particular, the broker can
339 manage at the same time several sessions working on different status/hints
340 formats. Of couse, there must be an agreement between the clients
341 and the tutors on the format of the data exchanged.
343 In our implementation the client does not trust the tutors hints:
344 being encoded as references to available tactics imply
345 that an \hbugs{} client, on receipt of an hint, simply try to reply the work
346 done by a tutor on the local copy of the proof. The application of the hint
347 can even fail to type check and the client copy of the proof can be left
348 undamaged after spotting the error. Note, however, that it is still
349 possible to implement a complex tutor that looks for a proof doing
351 send back to the client an hint whose argument is a witness (a trace) of
352 the proof found: the client applies the hint reconstructing (and checking
353 the correctness of) the proof from the witness, without having to
354 re-discover the proof itself.
356 An alternative implementation where the tutors are trusted would simply
357 send back to the client a new proof-status. Upong receiving the
358 proof-status, the client would just override its current proof status with
359 the suggested one. In the case of those clients which are implemented
360 using proof-objects (as the Coq proof-assistant, for instance), it is
361 still possible for the client to type-check the proof-object and reject
362 wrong hints. The systems that are not based on proof-objects
363 (as PVS, NuPRL, etc.), instead, have to trust the new proof-status. In this
364 case the \hbugs{} architecture needs at least to be extended with
365 clients-tutors autentication.
367 \paragraph{Registries}
368 Being central in the \hbugs{} architecture, the broker is also responsible
369 of housekeeping operations both for clients and tutors. These operations are
370 implemented using three different data structures called \emph{registries}:
371 clients registry, tutors registry and \musings{} registry.
373 In order to use the suggestion engine a client should register itself to the
374 broker and subscribe to one or more tutors. The registration phase is
375 triggered by the client using the \texttt{Register\_client} method of the
376 broker to send him an unique identifier and its base URI as a
377 \ws{}. After the registration, the client can use broker's
378 \texttt{List\_tutors} method to get a list of available tutors.
379 Eventually the client can subscribe to one or more of these using broker's
380 \texttt{Subscribe} method. Clients can also unregister from brokers using
381 \texttt{Unregister\_client} method.
383 The broker keeps track of both registered clients and clients' subscriptions
384 in the clients registry.
386 In order to be advertised to clients during the subscription phase, tutors
387 should register to the broker using the broker's \texttt{Register\_tutor}
388 method. This method is really similar to \texttt{Register\_client}:
389 tutors are required to send an unique identify and a base URI for their
391 Additionally tutors are required to send an human readable description of
392 their capabilities; this information could be used by client's user to
393 decide which tutors he needs to subscribe to. Like clients, tutors can
394 unregister from brokers using \texttt{Unregister\_broker} method.
396 Each time the client status change, the status is sent to the
397 broker using its \emph{Status} method. Using both clients registry (to
398 lookup client's subscription) and tutors registry (to check if some tutors
399 has unsubscribed), the broker is able to decide to which tutors the
400 new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
401 della possibilit\'a di avere un vero brocker che multiplexi le richieste
402 del tutor localizzando i servizi, etc.}
404 The forwarding operation is performed using the \texttt{Start\_musing}
405 method of the tutors, that is a request to start a new computation
406 (\emph{\musing{}}) on a given status. The return value of
407 \texttt{Start\_musing} is a
408 \musing{} identifier that is saved in the \musings{} registry along with
409 the identifier of the client that triggered the \musing{}.
411 As soon as a tutor completes an \musing{}, it informs the broker
412 using its \texttt{Musing\_completed} method; the broker can now remove the
413 \musing{} entry from the \musings{} registry and, depending on its outcome,
414 inform the client. In case of success one of the \texttt{Musing\_completed}
415 arguments is an hint to be sent to the client, otherwise there's no need to
416 inform him and the \texttt{Musing\_completed} method is called
417 just to update the \musings{} registry.
419 Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
420 stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
421 ovviamente ... CSC: ma a che serve???} is able to know, at each time,
422 which \musings{} are in execution on which tutor. This peculiarity is
423 exploited by the broker on invocation of Status method. Receiving a new
424 status from the client implies indeed that the previous status no longer
425 exists and all \musings{} working on it should be stopped: additionally to
426 the already described behaviour (i.e. starting new \musings{} on the
427 received status), the tutor\ednote{CSC: Ma sei veramente veramente sicuro?}
428 takes also care of stopping ongoing computation invoking
429 \texttt{Stop\_musing} tutors' method.
432 As already discussed, all \hbugs{} actors act as \wss{} offering one or more
433 services to neighbour actors. To grant as most accessibility as possible to
434 our \wss{} we have chosen to bind them using the HTTP/POST bindings
435 described in \cite{????}\footnote{Given that our proof assistant was
436 entirely developed in the Objective Caml language, we have chosen to
437 develop also \hbugs{} in that language in order to maximize code reuse. To
438 develop \wss{} in Objective Caml we have developed an auxiliary generic
439 library (\emph{O'HTTP}) that can be used to write HTTP 1.1 Web servers and
440 abstract over GET/POST parsing. This library supports different kinds of Web
441 servers architecture, including multi-process and multi-threaded ones.}.
444 Each tutor expose a \ws{} interface and should be able to work, not only for
445 many different clients referring to a common broker, but also for many
446 different brokers. The potential high number of concurrent clients imposes
447 a multi-threaded or multi-process architecture.
449 Our current implementation is based on a multi threaded architecture
450 exploiting the capabilities of the O'HTTP library. Each tutor is composed
451 by two thread always running plus
452 an additional thread for each running \musing{}. One thread is devoted to
453 listening for incoming \ws{} request; upon correct receiving requests it
454 pass the control to the second always-running thread which handle the pool
455 of running \musings{}. When a new \musing{} is requested, a new thread is
456 spawned to work them out; when a request to interrupt an old \musing{} is
457 received, the thread actually running them is killed freeing its
458 resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
459 ricordo male al problema dell'uccisione dei thread. Ora o si spiega
460 il motivo di questa architettura o si glissa/bluffa. Zack: cosa ti sembra
461 delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...
462 CSC: la motivazione per avere due thread always running e non due}
464 This architecture turns out to be scalable and allows the running threads
465 to share the cache of loaded (and type-checked) theorems.
466 As we will explain in Sect. \ref{tutors}, this feature turns out to be
467 really useful for tactics that rely on a huge but fixed set of lemmas,
468 as every reflexivite tactic.
470 The implementation of a tutor with the described architecture is not that
471 difficult having a language with good threading capabilities (as OCaml has)
472 and a pool of already implemented tactics (as gTopLevel has).
473 Still working with threads is known to be really error prone due to
474 concurrent programming intrinsic complexity. Moreover, there is a
475 non-neglectable part of code that needs to be duplicated in every tutor:
476 the code to register the tutor to the broker and to handle HTTP requests;
477 the code to manage the creation and termination of threads; and the code for
478 parsing the requests and serializing the answers. As a consequence we
479 have written a generic implementation of a tutor which is parameterized
480 over the code that actually propose the hint and some administrative
481 data (as the port the tutor will be listening to).
483 The generic tutor skeleton is really helpful in writing new tutors.
484 Nevertheless, the code obtained by converting existing tactics into tutors
485 is still quite repetitive: every tutor that wraps a tactic has to
486 instantiate its own copy of the proof-engine kernel and, for each request,
487 it has to override its status, guess the tactic arguments, apply the tactic
488 and, in case of success, send back an hint with the tactic name and the
489 chosen arguments. Of course, the complex part of the work is guessing the
490 right arguments. For the simple case of tactics that do not require
491 any argument, though, we are able to automatically generate the whole
492 tutor code given the tactic name. Concretely, we have written a
493 tactic-based tutor template and a script that parses an XML file with
494 the specification of the tutor and generates the tutor's code.
495 The XML file describes the tutor's port, the code to invoke the tactic,
496 the hint that is sent back upon successfull application and a
497 human readable explanation of the tactic implemented by the tutor.
499 \section{The Implemented \hbugs Tutors}
501 To test the \hbugs{} architecture and to assess the utility of a suggestion
502 engine for the end user, we have implemented several tutors. In particular,
503 we have investigated three classes of tutors:
505 \item \emph{Tutors for beginners}. These are tutors that implement tactics
506 which are neither computationally expensive nor difficult to understand:
507 an expert user can always understand if the tactic can be applied or not
508 withouth having to try it. For example, the following implemented tutors
509 belong to this class:
511 \item \emph{Assumption Tutor}: it ends the proof if the thesis is
512 equivalent\footnote{In our implementation, the equivalence relation
513 imposed by the logical framework is \emph{convertibility}. Two
514 expressions are convertible when they reduce to the same normal form.
515 Two ``equal'' terms depending on free variables can be non-convertible
516 since free variables stop the reduction. For example, $2x$ is convertible
517 with $(3-1)x$ because they both reduce to the same normal form
518 $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
519 already in normal form.}
520 to one of the hypotheses\footnote{
521 In some cases, expecially when non-trivial computations are involved,
522 the user is totally unable to figure out the convertibility of two terms.
523 In these cases the tutor becomes handy also for expert users.}.
524 \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
525 adsurdum} if one hypothesis is equivalent to $False$.
526 \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
527 suggests to apply the commutative property.
528 \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
529 the Constructor Tutor suggests to proceed in the proof by applying one
530 or more constructors when the goal thesis is an inductive type or a
531 proposition inductively defined according to the declarative
532 style\footnote{An example of a proposition that can be given in
533 declarative style is the $\le$ relation: $\le$ is the smallest relation
534 such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
535 that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
536 of $n \le n$ is simply the application of the first constructor to
537 $n$ and a proof of $n \le m$ is the application of the second
538 constructor to $n,m$ and a proof of $n \le m$.}.
539 Since disjunction, conjunction, existential quantification and
540 Leibniz equality are particular cases of inductive propositions,
541 all the other tutors of this class are instantiations of the
542 the Constructor tactic. Left and Right suggest to prove a disjunction
543 by proving its left/right member; Split reduces the proof of a
544 conjunction to the two proof of its members; Exists suggests to
545 prove an existential quantification by providing a
546 witness\footnote{This task is left to the user.}; Reflexivity proves
547 an equality whenever the two sides are convertible.
549 Beginners, when first faced with a tactic-based proof-assistant, get
550 lost quite soon since the set of tactics is large and their names and
551 semantics must be remembered by heart. Tutorials are provided to guide
552 the user step-by-step in a few proofs, suggesting the tactics that must
553 be used. We believe that our beginners tutors can provide an auxiliary
554 learning tool: after the tutorial, the user is not suddendly left alone
555 with the system, but she can experiment with variations of the proof given
556 in the tutorial as much as she like, still getting useful suggestions.
557 Thus the user is allowed to focus on learning how to do a formal proof
558 instead of wasting efforts trying to remember the interface to the system.
559 \item{Tutors for Computationally Expensive Tactics}. Several tactics have
560 an unpredictable behaviour, in the sense that it is unfeasible to understand
561 wether they will succeed or they will fail when applied and what will be
562 their result. Among them, there are several tactics either computationally
563 expensive or resources consuming. In the first case, the user is not
564 willing to try a tactic and wait for a long time just to understand its
565 outcome: she would prefer to keep on concentrating on the proof and
566 have the tactic applied in background and receive out-of-band notification
567 of its success. The second case is similar, but the tactic application must
568 be performed on a remote machine to avoid overloading the user host
569 with several concurrent resource consuming applications.
571 Finally, several complex tactics and in particular all the tactics based
572 on reflexive techniques depend on a pretty large set of definitions, lemmas
573 and theorems. When these tactics are applied, the system needs to retrieve
574 and load all the lemmas. Pre-loading all the material needed by every
575 tactic can quickly lead to long initialization times and to large memory
576 footstamps. A specialized tutor running on a remote machine, instead,
577 can easily pre-load the required theorems.
579 As an example of computationally expensive task, we have implemented
580 a tutor for the \emph{Ring} tactic \cite{ring_bouting}.
581 The tutor is able to prove an equality over a ring by reducing both members
582 to a common normal form. The reduction, which may require some time in
584 is based on the usual commutative, associative and neutral element properties
585 of a ring. The tactic is implemented using a reflexive technique, which
586 means that the reduction trace is not stored in the proof-object itself:
587 the type-checker is able to perform the reduction on-the-fly thanks to
588 the conversion rules of the system. As a consequence, in the library there
589 must be stored both the algorithm used for the reduction and the proof of
590 correctness of the algorithm, based on the ring axioms. This big proof
591 and all of its lemmas must be retrieved and loaded in order to apply the
592 tactic. The Ring tutor loads and cache all the required theorems the
593 first time it is conctacted.
594 \item{Intelligent Tutors}. Expert users can already benefit from the previous
595 class of tutors. Nevertheless, to achieve a significative production gain,
596 they need more intelligent tutors implementing domain-specific theorem
597 provers or able to perform complex computations. These tutors are not just
598 plain implementations of tactics or decision procedures, but can be
599 more complex software agents interacting with third-parties software,
600 such as proof-planners, CAS or theorem-provers.
602 To test the productivity impact of intelligent tutors, we have implemented
603 a tutor that is interfaced with the \helm{}
604 Search-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
605 is able to look for every theorem in the distributed library that can
606 be applied to proceed in the proof. Even if the tutor deductive power
607 is extremely limited\footnote{We do not attempt to check if the new goals
608 obtained applying a lemma can be authomatically proved or, even better,
609 auhomatically disproved to reject the lemma.}, it is not unusual for
610 the tutor to come up with precious hints that can save several minutes of
611 work that would be spent in proving again already proven results or
612 figuring out where the lemmas could have been stored in the library.
615 \section{Conclusions and Future Work}
617 In this paper we described a suggestion engine architecture for
618 proof-assistants: the client (a proof-assistant) sends the current proof
619 status to several distributed \wss{} (called tutors) that try to progress
620 in the proof and, in case of success, send back an appropriate hint
621 (a proof-plan) to the user. The user, that in the meantime was able to
622 reason and progress in the proof, is notified with the hints and can decide
623 to apply or ignore them. A broker is provided to decouple the clients and
624 the tutors and to allow the client to locate and invoke the available remote
625 services. The whole architecture is an instance of the MONET architecture
626 for Mathematical \wss{}.
628 A running prototype has been implemented as part of the
629 \helm{} project \cite{}
630 and we already provide several tutors. Some of them are simple tutors that
631 try to apply one or more tactics of the \helm{} Proof-Engine, which is also
632 our client. We also have a much more complex tutor that is interfaced
633 with the \helm{} Search-Engine and looks for lemmas that can be directly
636 We have many plan for further developing both the \hbugs{} architecture and
637 our prototype. Interesting results could be obtained
638 augmenting the informative content of each suggestion. We can for example
639 modify the broker so that also negative results are sent back to the client.
640 Those negative suggestions could be reflected in the user interface by
641 deactivating commands to narrow the choice of tactics available to the user.
642 This approach could be interesting expecially for novice users, but require
643 the client to trust other actors a bit more than in the current approach.
645 We plan also to add some rating mechanism to the architecture. A first
646 improvement in this direction could be to distinguish between hints that, when
647 applied, are able to completely close one or more goals and
648 tactics that progress in the proof by reducing one or more goals to new goals:
649 the new goals could be false and the proof can be closed only by backtraking.
651 Other heuristics and/or measures could be added to rate
652 hints and show them to the user in a particular order: an interesting one
653 could be a measure that try to minimize the size of the generated proof,
654 privileging therefore non-overkilling solutions \cite{ring}.
656 We are also considering to follow the \OmegaAnts{} path more closely adding
657 ``recursion'' to the system so that proof status resulting from the
658 application of old hints are cached somewhere and could be used as a starting
659 point for new hint searches. The approach is interesting, but it represents
660 a big shift towards automatic theorem proving: thus we must consider if it is
661 worth the effort given the increasing availability of automation in proof
662 assistants' tactics and the ongoing development of \wss{} based on
663 already existent and well developed theorem provers.
665 Even if not strictly part of the \hbugs{} architecture, the graphical user
666 interface (GUI) of our prototype needs a lot of improvement if we would like
667 it to be really usable by novices. In particular, the user is too easily
668 distracted by the tutor's hints that are ``pushed'' to her.
670 Our \wss{} still lack a real integration in the MONET architecture,
671 since we do not provide the different ontologies to describe our problems,
672 solutions, queries and services. In the short term, completing this task
673 could provide a significative feedback to the MONET consortium and would
674 enlarge the current set of available MONET actors on the Web. In the long
675 term, new more intelligent tutors could be developed on top of already
676 existent MONET \wss{}.
678 To conclude, \hbugs{} is a nice experiment meant to understand whether the
679 current \wss{} technology is mature enough to have a concrete and useful
680 impact on the daily work of users of proof-assistants. So far, only the tutor
681 that is interfaced with the \helm{} Search-Engine has effectively increased
682 the productivity of experts users. The usefullness of the tutors developed for
683 beginners, instead, need further assessment.
685 \begin{thebibliography}{01}
687 % \bibitem{ALF} The ALF family of proof-assistants:\\
688 % {\tt http://www.cs.chalmers.se/ComputingScience/Research/\\Logic/implementation.mhtml}
690 % \bibitem{Coq} The Coq proof-assistant:\\
691 % {\tt http://coq.inria.fr/}
693 % \bibitem{FORMAVIE} The Formavie project:\\
694 % {\tt http://http://www-sop.inria.fr/oasis/Formavie/}
696 % \bibitem{EHELM} The HELM project:\\
697 % {\tt http://www.cs.unibo.it/helm/}
699 % \bibitem{MATHWEB} The MathWeb project:\\
700 % {\tt http://www.mathweb.org/}
702 % \bibitem{PCOQ} The PCoq project:\\
703 % {\tt http://www-sop.inria.fr/lemme/pcoq/}
705 % \bibitem{HELM} A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
706 % Towards a library of formal mathematics. Panel session of
707 % the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLS'2000),
708 % Portland, Oregon, USA.
710 % \bibitem{Ring} S. Boutin. Using reflection to build efficient and certified
711 % decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS'97,
712 % volume 1281. LNCS, Springer-Verlag, 1997.
714 % \bibitem{YANNTHESIS} Y.Coscoy. \emph{Explication textuelle de preuves pour le
715 % Calcul des Constructions Inductives}, PhD. Thesis, Universit\'e de Nice-Sophia
718 % \bibitem{ALFA} T. Hallgreen, Aarne Ranta. An Extensible Proof Text Editor.
719 % Presented at LPAR2000.
721 % \bibitem{Necula} G. Necula, P. Lee. Safe Kernel Extensions Without Run-Time
722 % Checking. Presented at OSDI'96, October 1996.
724 % \bibitem{Necula2} G. Necula, P. Lee. Efficient Representation and Validation of Proofs. Presented at LICS'98, June 1998
726 % \bibitem{Werner} B. Werner. \emph{Une Th\'eorie des Constructions Inductives},
727 % PhD. Thesis, Universit\'e Paris VII, May 1994.
729 \end{thebibliography}