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 Via di 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 \cite{MONET},
84 following the guidelines \ednote{guidelines non e' molto appropriato, dato che
85 il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers
86 approach, is working on the development of a framework aimed at providing a
87 set of software tools for the advertisement and discovering of mathematical
89 %CSC This framework turns out to be strongly based on both \wss{} and brokers.
91 Several groups have already developed \wss{} providing both computational and
92 reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
93 dalle conferenze calculemus}: the formers are implemented on top of
94 Computer Algebra Systems; the latters provide interfaces to well-known
95 theorem provers. Proof-planners, proof-assistants, CAS and
96 domain-specific problem solvers are natural candidates to be client of these
97 services. Nevertheless, so far the number of examples in the literature has
98 been extremely low and the concrete benefits are still to be assessed.
100 In this paper we present an architecture, namely \hbugs{}, implementing a
101 \emph{suggestion engine} for the proof assistant developed on behalf of the
102 \helm{} project. 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 distribute 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 Both the broker and the tutors are instances of the homonymous entities of
111 A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
112 which provided similar functionalities to the
113 \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
114 between \hbugs{} and \OmegaAnts{} is that the latter is based on a
115 black-board architecture and it is not implemented using \wss{} and
116 brokers. Other differences will be detailed in Sect. \ref{conclusions}.
118 In Sect. \ref{architecture} we present the architecture of \hbugs{}.
119 Further implementation details are given in Sect. \ref{implementation}.
120 Sect. \ref{tutors} is an overview of the tutors that have been implemented.
121 As usual, the paper ends with the conclusions and future works.
124 {CSC: Non so se/dove mettere queste parti.
125 Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
126 non e' molto utile, ma la seconda sugli usi tipici di proof assistant
129 Despite of that the proof assistant case seems to be well suited to
130 investigate the usage of many different mathematical \wss{}. Indeed: most
131 proof assistants are still based on non-client/server architectures, are
132 application-centric instead of document-centric, offer a scarce level of
133 automation leaving entirely to the user the choice of which macro (usually
134 called \emph{tactic}) to use in order to make progress in a proof.
136 The average proof assistant can be, for example, a client of a \ws{}\
137 interfacing a specific or generic purpose theorem prover, or a client of a
138 \ws{} interfacing a CAS to simplify expressions in a particular mathematical
142 \section{Architecture}
144 \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
146 The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
147 different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
148 Each actor present one or more \ws{} interfaces to its neighbours \hbugs{}
151 In this section we will detail the role and requirements of each kind of
152 actors and discuss about the correspondencies between them and the MONET
153 entities described in \cite{MONET-Overview}.
156 An \hbugs{} client is a software component able to produce \emph{proof
157 status} and to consume \emph{hints}.
159 \ednote{Zack: "status" ha il plurale? CSC: no}
160 A proof status is a representation of an incomplete proof and is supposed to
161 be informative enough to be used by an interactive proof assistant. No
162 additional requirements exist on the proof status, but there should be an
163 agreement on its format between clients and tutors. An hint is a
164 representation\ednote{non c'\'e un sinonimo pi\'u carino?}
165 of a step that can be performed in order to proceed in an
166 incomplete proof. Usually it represents a reference to a tactic available
167 on some proof assistant along with an instantiation for its formal
168 parameters. More structured hints can also be used: an hint can be
169 as complex as a whole proof-plan.
171 Clients act both as \ws{} provider and requester (using W3C's terminology
172 \cite{ws-glossary}). They act as providers for the broker (to receive hints)
173 and as requesters (to submit new status). Clients
174 additionally use broker service to know which tutors are available and to
175 subscribe to one or more of them.
177 Usually, when the role of client is taken by an interactive proof assistant,
178 new status are sent to the broker as soon as the proof change (e.g. when the
179 user applies a tactic or when a new proof is started) and hints are shown to
180 the user be the means of some effect in the user interface (e.g. popping a
181 dialog box or enlightening a tactic button).
183 \hbugs{} clients act as MONET clients and ask broker to provide access to a
184 set of services (the tutors). \hbugs{} has no actors corresponding to
185 MONET's Broker Locating Service (since the client is supposed to know the
186 URI of at least one broker) and Mathematical Object Manager (since proof
187 status are built on the fly and not stored).
190 \hbugs{} brokers are the key actors of the \hbugs{} architecture since they
191 act as intermediaries between clients and tutors. They behave as \ws{}
192 providers and requesters for \emph{both} clients and tutors.
194 With respect to client, a broker act as \ws{} provider, receiving the
195 proof status and forwarding it to one or more tutors.
196 It also acts as a \ws{} requester sending
197 hints to client as soon as they are available from the tutors.
199 With respect to tutors, the \ws{} provider role is accomplished by receiving
200 hints as soon as they are produced; as a requester one is accomplished
201 by requesting computations (\emph{musings} in \hbugs{} terminology) on
202 status received by clients and by stopping already late but still
204 \ednote{Sta frase va comunque riscritta perch\'e non si capisce una mazza}.
206 Additionally brokers keep track of available tutors and clients
209 \hbugs{} brokers act as MONET brokers implementing the following components:
210 Client Manager, Service Registry Manager (keeping track of available
211 tutors), Planning Manager (chosing the available tutors among the ones to
212 which the client is subscribed), Execution Manager. \ednote{non e' chiaro se
213 in monet le risposte siano sincrone o meno, se cosi' fosse dobbiamo
214 specificare che nel nostro caso non lo sono}
217 Tutors are software component able to consume proof status producing hints.
218 \hbugs{} doesn't specify by which means hints should be produced: tutors can
219 use any means necessary (heuristics, external theorem prover or CAS, ...).
220 The only requirement is that exists an agreement on the formats of proof
223 Tutors act both as \ws{} providers and requesters for the broker. As
224 providers, they wait for commands requesting to start a new \musing{} on
225 a given proof status or to stop an old, out of date, \musing{}. As
226 requesters, they signal to the broker the end of a \musing{} along with its
227 outcome (an hint in case of success or a notification of failure).
229 \hbugs{} tutors act as MONET services.
231 \section{Implementation details}
232 \label{implementation}
233 \ednote{Zack: l'aspetto grafico di questa parte e' un po' peso, possiamo
234 aggiungere varie immagini volendo, e.g.: schema dei thread di un tutor, sample
235 code di un tutor generato automaticamente}
236 \ednote{Zack: ho cambiato idea riguardo a questa parte, mettere la lista delle
237 interfacce di client/broker/... mi sembrava sterile e palloso. Di conseguenza ho
238 messo i punti chiave dell'implementazione, dimmi cosa te ne pare ...}
239 In this section we present some of the most relevant implementation details of
240 the \hbugs{} architecture.
243 \paragraph{Proof status}
244 In our implementation of the \hbugs{} architecture we used the proof
245 assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
246 client. Thus we have implemented serialization/deserialization capabilities
247 fot its internal status. In order to be able to describe \wss{} that
248 exchange status in WSDL using the XML Schema type system, we have chosen an
249 XML format as the target format for the serialization.
251 A schematic representation of the gTopLevel internal status is depicted in
252 Fig. \ref{status}. Each proof is representated by a tuple of four elements:
253 \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
255 \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
259 \item[uri]: an URI chosen by the user at the beginning of the proof
260 process. Once (and if) proved, that URI will globally identify the term
261 inside the \helm{} library (given that the user decides to save it).
262 \item[thesis]: the thesis of the ongoing proof
263 \item[proof]: the current incomplete proof tree. It can contain
264 \emph{metavariables} (holes) that stands for the parts of the proof
265 that are still to be completed. Each metavariables appearing in the
266 tree references one element of the metavariables environment
268 \item[metasenv]: the metavariables environment is a list of
269 \emph{goals} (unproved conjectures).
270 In order to complete the proof, the user has to instantiate every
271 metavariable in the proof with a proof of the corresponding goal.
272 Each goal is identified by an unique identifier and has a context
273 and a type ( the goal thesis). The context is a list of named
274 hypotheses (declarations and definitions). Thus the context and the goal
275 thesis form a sequent, which is the statement of the proof that will
276 be used to instatiate the metavariable occurrences.
279 Each of these information is represented in XML as described in
280 \cite{csc-thesis}. Additionally, an \hbugs{} status carry the unique
281 identifier of the current goal, which is the goal the user is currently
282 focused on. Using this value it is possible to implement different client
283 side strategies: the user could ask the tutors to work on the goal
284 she is considering or to work on the other ``background'' goals.
287 An hint in the \hbugs{} architecture should carry enough information to
288 permit the client to progress in the current proof. In our
289 implementation each hint corresponds to either one of the tactics available
290 to the user in gTopLevel (together with its actual arguments) or a set
291 of alternative suggestions (a list of hints).
293 For tactics that don't require any particular argument (like tactics that
294 apply type constructors or try to automatically conclude equality goals)
295 only the tactic name is represented in the hint. For tactics that need terms
296 as arguments (for example the \emph{Apply} tactic) the hint includes a
297 textual representation of them, using the same representation used by the
298 interactive proof assistant when querying user for terms. In order to be
299 trasmitted between \wss, hints are serialized in XML.
301 Actually it is also possible for a tutor to return more hints at once,
302 grouping them in a particular XML element.
303 This feature turns out to be particulary useful for the
304 \emph{searchPatternApply} tutor (Sect. \ref{tutors}) that
305 query a term database and return to the client a list of all terms that
306 could be used to complete the proof. This particular hint is encoded as a
307 list of Apply hints, each of them having one of the results as term
310 We would like to stress that the \hbugs{} architecture has no dependency
311 on either the hint or the status representation: the only message parts
312 that are fixed are those representing the administrative messages
313 (the envelops in the \wss terminology). In particular, the broker can
314 manage at the same time several sessions working on different status/hints
315 formats. Of couse, there must be an agreement between the clients
316 and the tutors on the format of the data exchanged.
318 In our implementation the client does not trust the tutors' hints:
319 being encoded as references to available tactics imply
320 that an \hbugs{} client, on receipt of an hint, simply try to reply the work
321 done by a tutor on the local copy of the proof. The application of the hint
322 can even fail to type check and the client copy of the proof can be left
323 undamaged after spotting the error. Note, however, that it is still
324 possible to implement a complex tutor that looks for a possible proof and
325 send back to the client an hint whose argument is a witness (a trace) of
326 the proof found: the client applies the hint reconstructing (and checking
327 the correctness of) the proof from the witness, without having to
328 re-discover the proof itself.
330 An alternative implementation where the tutors are trusted would simply
331 send back to the client a new proof-status. Upong receiving the
332 proof-status, the client would just override its current proof status with
333 the suggested one. In the case of those clients which are implemented
334 using proof-objects (as the Coq proof-assistant, for instance), it is
335 still possible for the client to type-check the proof-object and reject
336 wrong hints. The systems that are not based on proof-objects
337 (as PVS, NuPRL, etc.), instead, have to trust the new proof-status. In this
338 case the \hbugs{} architecture needs to be extended with clients-tutors
341 \paragraph{Registries}
342 Being central in the \hbugs{} architecture, the broker is also responsible
343 of accounting operations both for clients and tutors. These operations are
344 implemented using three different data structures called \emph{registries}:
345 clients registry, tutors registry and \musings{} registry.
347 In order to use the suggestion engine a client should register itself to the
348 broker and subscribe to one or more tutors. The registration phase is
349 triggered by the client using the \texttt{Register\_client} method of the
350 broker to send him an unique identifier and its base URI as a
351 \ws{}. After the registration, the client can use broker's
352 \texttt{List\_tutors} method to get a list of available tutors.
353 Eventually\ednote{CSC: Vuoi veramente dire eventually qui?} the
354 client can subscribe to one or more of these using broker's \emph{Subscribe}
355 method. Clients can also unregister from brokers using
356 \texttt{Unregister\_client} method.
358 The broker keeps track of both registered clients and clients' subscriptions
359 in the clients registry.
361 In order to be advertised to clients during the subscription phase, tutors
362 should register to the broker using broker's \texttt{Register\_tutor}
363 method. This method is really similar to the \texttt{Register\_client}
364 one: tutors are required to send an unique identify and a base URI for
366 Additionally tutors are required to send an human readable description of
367 their capabilities; this information could be used by client's user to
368 decide which tutors he needs to subscribe to. Like clients, tutors can
369 unregister from brokers using \texttt{Unregister\_broker} method.
371 Track of available tutors is kept in the tutors
372 registry.\ednote{Non si mette mai un paragrafo lungo meno di una linea!}
374 Each time the client status change, the status is sent to the
375 broker using its \emph{Status} method. Using both clients registry (to
376 lookup client's subscription) and tutors registry (to check if some tutors
377 has unsubscribed), the broker is able to decide to which tutors the
378 new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
379 della possibilit\'a di avere un vero brocker che multiplexi le richieste
380 del tutor localizzando i servizi, etc.}
382 The forwarding operation is performed using tutors' \texttt{Start\_musing}
383 method, that is a request to start a new computation (\emph{\musing{}}) on a
384 given status. The return value for \texttt{Start\_musing} method is a
385 \musing{} identifier that is saved in the \musings{} registry along with
386 the identifier of the client that triggered the starting of the \musing{}.
388 As soon as a \musing{} is completed, the owning tutor informs the broker
389 using its \texttt{Musing\_completed} method; the broker can now remove the
390 \musing{} entry from the \musings{} registry and, depending on its outcome,
391 inform the client. In case of success one of the \texttt{Musing\_completed}
392 arguments is an hint to be sent to the client, otherwise there's no need to
393 inform him and the \texttt{Musing\_completed} method is called
394 just to update the \musings{} registry.
396 Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
397 stai delirando?} is able to know, at each time,
398 which \musings{} are in execution on which tutor. This peculiarity is
399 exploited by the broker on invocation of Status method. Receiving a new
400 status from the client imply indeed that the previous status no longer
401 exists and all \musings{} working on it should be stopped: additionally to
402 the already described behaviour (i.e. starting new \musings{} on the
403 received status), the tutor takes also care of stopping ongoing computation
404 invoking \texttt{Stop\_musing} tutors' method.
407 As already discussed, all \hbugs{} actors act as \wss{} offering one or more
408 services to neighbour actors. To grant as most accessibility as possible to
409 our \wss{} we have chosen to bind them using the HTTP/POST bindings
410 described in \cite{????}\footnote{Given that our proof assistant was
411 entirely developed in the Objective Caml language, we have chosen to
412 develop also \hbugs{} in that language in order to maximize code reuse. To
413 develop \wss{} in Objective Caml we have developed an auxiliary generic
414 library (\emph{O'HTTP}) that can be used to write HTTP 1.1 web servers and
415 abstract over GET/POST parsing. This library supports different kinds of web
416 servers architecture, including multi-process and multi-threaded ones.}.
419 Each tutor expose a \ws{} interface and should be able to work, not only for
420 many different clients referring to a common broker, but also for many
421 different brokers. The potential high number of concurrent clients imposes
422 a multi-threaded or multi-process architecture.
424 Our current implementation is based on a multi threaded architecture
425 exploiting the capabilities of the O'HTTP library. Each tutor is composed
426 by two thread always running plus
427 an additional thread for each running \musing{}. One thread is devoted to
428 listening for incoming \ws{} request; upon correct receiving requests it
429 pass the control to the second always-running thread which handle the pool
430 of running \musings{}. When a new \musing{} is requested, a new thread is
431 spawned to work them out; when a request to interrupt an old \musing{} is
432 received, the thread actually running them is killed freeing its
433 resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
434 ricordo male al problema dell'uccisione dei thread. Ora o si spiega
435 il motivo di questa architettura o si glissa/bluffa.}
437 This architecture turns out to be scalable and allows the running threads
438 to share the cache of loaded (and type-checked) theorems.
439 As we will explain in Sect. \ref{tutors}, this feature turns out to be
440 really useful for tactics that rely on a huge but fixed set of lemmas,
441 as every reflexivite tactic.
443 The implementation of a tutor with the described architecture is not that
444 difficult having a language with good threading capabilities (as OCaml has)
445 and a pool of already implemented tactics (as gTopLevel has).
446 Still working with threads is known to be really error prone due to
447 concurrent programming intrinsic complexity. Moreover, there is a
448 non-neglectable part of code that needs to be duplicated in every tutor:
449 the code to register the tutor to the broker and to handle HTTP requests;
450 the code to manage the creation and termination of threads; and the code for
451 parsing the requests and serializing the answers. As a consequence we
452 have written a generic implementation of a tutor which is parameterized
453 over the code that actually propose the hint and some administrative
454 data (as the port the tutor will be listening to).
456 The generic tutor skeleton is really helpful in writing new tutors.
457 Nevertheless, the code obtained by converting existing tactics into tutors
458 is still quite repetitive: every tutor that wraps a tactic has to
459 instantiate its own copy of the proof-engine kernel and, for each request,
460 it has to override its status, guess the tactic arguments, apply the tactic
461 and, in case of success, send back an hint with the tactic name and the
462 chosen arguments. Of course, the complex part of the work is guessing the
463 right arguments. For the simple case of tactics that do not require
464 any argument, though, we are able to automatically generate the whole
465 tutor code given the tactic name. Concretely, we have written a
466 tactic-based tutor template and a script that parses an XML file with
467 the specification of the tutor and generates the tutor's code.
468 The XML file holds the tutor's port, the code to invoke the tactic,
469 the hint that is sent back upon successfull application and a
470 human readable explanation of the tactic implemented by the tutor.
472 \section{The Implemented \hbugs Tutors}
474 To test the \hbugs{} architecture and to assess the utility of a suggestion
475 engine for the end user, we have implemented several tutors. In particular,
476 we have investigated three classes of tutors:
478 \item \emph{Tutors for beginners}. These are tutors that implement tactics
479 which are neither computationally expensive nor difficult to understand:
480 an expert user can always understand if the tactic can be applied or not
481 withouth having to try it. For example, the following implemented tutors
482 belong to this class:
484 \item \emph{Assumption Tutor}: it ends the proof if the thesis is
485 equivalent\footnote{In our implementation, the equivalence relation
486 imposed by the logical framework is \emph{convertibility}. Two
487 expressions are convertible when they reduce to the same normal form.
488 Two ``equal'' terms depending on free variables can be non-convertible
489 since free variables stop the reduction. For example, $2x$ is convertible
490 with $(3-1)x$ because they both reduce to the same normal form
491 $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
492 already in normal form.}
493 to one of the hypotheses\footnote{
494 In some cases, expecially when non-trivial computations are involved,
495 the user is totally unable to figure out the convertibility of two terms.
496 In these cases the tutor becomes handy also for expert users.}.
497 \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
498 adsurdum} if one hypothesis is equivalent to $False$.
499 \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
500 suggests to apply the commutative property.
501 \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
502 the Constructor Tutor suggests to proceed in the proof by applying one
503 or more constructors when the goal thesis is an inductive type or a
504 proposition inductively defined according to the declarative
505 style\footnote{An example of a proposition that can be given in
506 declarative style is the $\le$ relation: $\le$ is the smallest relation
507 such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
508 that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
509 of $n \le n$ is simply the application of the first constructor to
510 $n$ and a proof of $n \le m$ is the application of the second
511 constructor to $n,m$ and a proof of $n \le m$.}.
512 Since disjunction, conjunction, existential quantification and
513 Leibniz equality are particular cases of inductive propositions,
514 all the other tutors of this class are restrictions of the
515 the Constructor tactic: Left and Right suggest to prove a disjunction
516 by proving its left/right member; Split reduces the proof of a
517 conjunction to the two proof of its members; Exists suggests to
518 prove an existential quantification by providing a
519 witness\footnote{This task is left to the user.}; Reflexivity proves
520 an equality whenever the two sides are convertible.
522 Beginners, when first faced with a tactic-based proof-assistant, get
523 lost quite soon since the set of tactics is large and their names and
524 semantics must be remembered by heart. Tutorials are provided to guide
525 the user step-by-step in a few proofs, suggesting the tactics that must
526 be used. We believe that our beginners tutors can provide an auxiliary
527 learning tool: after the tutorial, the user is not suddendly left alone
528 with the system, but she can experiment with variations of the proof given
529 in the tutorial as much as she like, still getting useful suggestions.
530 Thus the user is allowed to focus on learning how to do a formal proof
531 instead of wasting efforts trying to remember the interface to the system.
532 \item{Tutors for Computationally Expensive Tactics}. Several tactics have
533 an unpredictable behaviour, in the sense that it is unfeasible to understand
534 wether they will succeed or they will fail when applied and what will be
535 their result. Among them, there are several tactics either computationally
536 expensive or resources consuming. In the first case, the user is not
537 willing to try a tactic and wait for a long time just to understand its
538 outcome: she would prefer to keep on concentrating on the proof and
539 have the tactic applied in background and receive out-of-band notification
540 of its success. The second case is similar, but the tactic application must
541 be performed on a remote machine to avoid overloading the user host
542 with several concurrent resource consuming applications.
544 Finally, several complex tactics and in particular all the tactics based
545 on reflexive techniques depend on a pretty large set of definitions, lemmas
546 and theorems. When these tactics are applied, the system needs to retrieve
547 and load all the lemmas. Pre-loading all the material needed by every
548 tactic can quickly lead to long initialization times and to large memory
549 footstamps. A specialized tutor running on a remote machine, instead,
550 can easily pre-load the required theorems.
552 As an example of computationally expensive task, we have implemented
553 a tutor for the \emph{Ring} tactic. The tutor is able to prove an equality
554 over a ring by reducing both members to a common normal form. The reduction,
555 which may require some time in complex cases,
556 is based on the usual commutative, associative and neutral element properties
557 of a ring. The tactic is implemented using a reflexive technique, which
558 means that the reduction trace is not stored in the proof-object itself:
559 the type-checker is able to perform the reduction on-the-fly thanks to
560 the conversion rules of the system. As a consequence, in the library there
561 must be stored both the algorithm used for the reduction and the proof of
562 correctness of the algorithm, based on the ring axioms. This big proof
563 and all of its lemmas must be retrieved and loaded in order to apply the
564 tactic. The Ring tutor loads and cache all the required theorems the
565 first time it is conctacted.
566 \item{Intelligent Tutors}. Expert users can already benefit from the previous
567 class of tutors. Nevertheless, to achieve a significative production gain,
568 they need more intelligent tutors implementing domain-specific theorem
569 provers or able to perform complex computations. These tutors are not just
570 plain implementations of tactics or decision procedures, but can be
571 more complex software agents interacting with third-parties software,
572 such as proof-planners, CAS or theorem-provers.
574 To test the productivity impact of intelligent tutors, we have implemented
575 a tutor that is interfaced with the HELM
576 Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
577 is able to look for every theorem in the distributed library that can
578 be applied to proceed in the proof. Even if the tutor deductive power
579 is extremely limited\footnote{We do not attempt to check if the new goals
580 obtained applying a lemma can be authomatically proved or, even better,
581 auhomatically disproved to reject the lemma.}, it is not unusual for
582 the tutor to come up with precious hints that can save several minutes of
583 work that would be spent in proving again already proven results or
584 figuring out where the lemmas could have been stored in the library.
590 \begin{thebibliography}{01}
592 % \bibitem{ALF} The ALF family of proof-assistants:\\
593 % {\tt http://www.cs.chalmers.se/ComputingScience/Research/\\Logic/implementation.mhtml}
595 % \bibitem{Coq} The Coq proof-assistant:\\
596 % {\tt http://coq.inria.fr/}
598 % \bibitem{FORMAVIE} The Formavie project:\\
599 % {\tt http://http://www-sop.inria.fr/oasis/Formavie/}
601 % \bibitem{EHELM} The HELM project:\\
602 % {\tt http://www.cs.unibo.it/helm/}
604 % \bibitem{MATHWEB} The MathWeb project:\\
605 % {\tt http://www.mathweb.org/}
607 % \bibitem{PCOQ} The PCoq project:\\
608 % {\tt http://www-sop.inria.fr/lemme/pcoq/}
610 % \bibitem{HELM} A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
611 % Towards a library of formal mathematics. Panel session of
612 % the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLS'2000),
613 % Portland, Oregon, USA.
615 % \bibitem{Ring} S. Boutin. Using reflection to build efficient and certified
616 % decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS'97,
617 % volume 1281. LNCS, Springer-Verlag, 1997.
619 % \bibitem{YANNTHESIS} Y.Coscoy. \emph{Explication textuelle de preuves pour le
620 % Calcul des Constructions Inductives}, PhD. Thesis, Universit\'e de Nice-Sophia
623 % \bibitem{ALFA} T. Hallgreen, Aarne Ranta. An Extensible Proof Text Editor.
624 % Presented at LPAR2000.
626 % \bibitem{Necula} G. Necula, P. Lee. Safe Kernel Extensions Without Run-Time
627 % Checking. Presented at OSDI'96, October 1996.
629 % \bibitem{Necula2} G. Necula, P. Lee. Efficient Representation and Validation of Proofs. Presented at LICS'98, June 1998
631 % \bibitem{Werner} B. Werner. \emph{Une Th\'eorie des Constructions Inductives},
632 % PhD. Thesis, Universit\'e Paris VII, May 1994.
634 \end{thebibliography}