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