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