1 \documentclass[runningheads]{llncs}
7 % \myincludegraphics{filename}{place}{width}{caption}{label}
8 \newcommand{\myincludegraphics}[5]{
11 \includegraphics[width=#3]{eps/#1.eps}
18 %\usepackage[show]{ed}
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}
33 Claudio Sacerdoti Coen\thanks{Partially supported by `MoWGLI: Math on the Web, Get it by Logic and Interfaces', EU IST-2001-33562} \and
34 Stefano Zacchiroli\thanks{Partially supported by `MyThS: Models and Types for Security in Mobile Distributed Systems', EU FET-GC IST-2001-32617}}
37 Department of Computer Science\\
38 University of Bologna\\
39 Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
40 \email{sacerdot@cs.unibo.it}
42 Department of Computer Science\\
43 \'Ecole Normale Sup\'erieure\\
44 45, Rue d'Ulm, F-75230 Paris Cedex 05, FRANCE\\
45 \email{zack@cs.unibo.it}
55 We present a planning broker and several Web-Services for automatic deduction.
56 Each Web-Service implements one of the tactics usually available in
57 interactive proof-assistants. When the broker is submitted a ``proof status''
58 (an incomplete proof tree and a focus on an open goal) it dispatches the proof
59 to the Web-Services, collects the successful results, and send them back to
60 the client as ``hints'' as soon as they are available.
62 In our experience this architecture turns out to be helpful both for
63 experienced users (who can take benefit of distributing heavy computations)
64 and beginners (who can learn from it).
67 \section{Introduction}
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 consequence, 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 is to provide a further level of stable services (called
81 \emph{brokers}) that behave as common gateways/addresses for client
82 applications to access a wide variety of services and abstract over them.
84 Since the \emph{Declaration of Linz}, the MONET
85 Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}}
86 is working on the development of a framework, based on the
87 \wss{}/brokers approach, aimed at providing a set of software tools for the
88 advertisement and the discovery of mathematical \wss{}.
89 %CSC This framework turns out to be strongly based on both \wss{} and brokers.
91 Several groups have already developed software bus and
92 services\footnote{The most part of these systems predate the development of
93 \wss. Those systems whose development is still active are slowly being
94 reimplemented as \wss.} providing both computational and reasoning
95 capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of
96 Computer Algebra Systems; the second ones provide interfaces to well-known
98 Proof-planners, proof-assistants, CAS and
99 domain-specific problem solvers are natural candidates to be clients of these
100 services. Nevertheless, so far the number of examples in the literature has
101 been insufficient to fully assess the concrete benefits of this framework.
103 In this paper we present an architecture, namely \hbugs{}, implementing a
104 \emph{suggestion engine} for the proof assistant developed on behalf of the
105 \helm{}\footnote{Hypertextual Electronic Library of Mathematics,
106 \url{http://helm.cs.unibo.it}} project
107 \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to
108 suggest possible ways to proceed in a proof. The tutors are orchestrated
109 by a broker (a \ws{} itself) that is able to dispatch a proof
110 status from a client (the proof-assistant) to the tutors;
111 each tutor tries to make progress in the proof and, in case
112 of success, notifies the client that shows an \emph{hint} to the user.
113 The broker is an instance of the homonymous entity of the MONET framework.
114 The tutors are MONET services. Another \ws{} (which is not described in this
115 paper and which is called Getter \cite{zack}) is used to locate and download
116 mathematical entities; the Getter plays the role of the Mathematical Object
117 Manager of the MONET framework.
119 A precursor of \hbugs{} is the \OmegaAnts{} project
120 \cite{omegaants1,omegaants2}, which provided similar functionalities to the
121 \Omegapp{} proof-planner \cite{omega}. The main architectural difference
122 between \hbugs{} and \OmegaAnts{} is that the latter is based on a
123 black-board architecture and it is not implemented using \wss{} and
126 In Sect. \ref{architecture} we present the architecture of \hbugs{}.
127 A usage session is shown in Sect. \ref{usage}.
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 final section of this paper is devoted to conclusions and future works.
132 \section{An \hbugs{} Bird's Eye View}
134 \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
136 The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
137 different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
138 Each actor present one or more \ws{} interfaces to its neighbors \hbugs{}
141 In this section we detail the role and requirements of each kind of
142 actors and discuss about the correspondences between them and the MONET
143 entities described in \cite{MONET-Overview}.
144 Due to lack of space, we cannot compare our framework to similar proposals, as
145 the older and more advanced \Omegapp{} system. The study of the
146 correspondences with MONET is well motivated by the fact that the MONET
147 framework is still under development and that our implementation is one of the
148 first experiments in \ws-based distributed reasoning. On the other hand, the
149 comparison with \Omegapp{} is less interesting since the functionalities we
150 provide so far are clearly a subset of the \OmegaAnts ones.
153 An \hbugs{} client is a software component able to produce \emph{proof
154 status} and to consume \emph{hints}.
156 A proof status is a representation of an incomplete proof and is supposed to
157 be informative enough to be used by an interactive proof assistant. No
158 additional requirements exist on the proof status, but there should be an
159 agreement on its format between clients and tutors. A hint is an
160 encoding of a step that can be performed in order to proceed in an
161 incomplete proof. Usually it represents a reference to a tactic available
162 on some proof assistant along with an instantiation for its formal
163 parameters. More structured hints can also be used: a hint can be
164 as complex as a whole proof-plan.
166 Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
167 providers and requesters, see Fig. \ref{interfaces}. They act as providers
168 for the broker (to receive hints) and as requesters (to submit new status).
169 Clients additionally use broker services to know which tutors are available
170 and to subscribe to one or more of them.
172 Usually, when the client role is taken by an interactive proof assistant,
173 new status are sent to the broker as soon as the proof change (e.g. when the
174 user applies a tactic or when a new proof is started) and hints are shown to
175 the user by the means of some effects in the user interface (e.g. popping a
176 dialog box or enlightening a tactic button).
178 \hbugs{} clients act as MONET clients and ask brokers to provide access to a
179 set of services (the tutors). \hbugs{} has no actors corresponding to
180 MONET's Broker Locating Service (since the client is supposed to know the
181 URI of at least one broker). The \hbugs{} clients and tutors contact the
182 Getter (a MONET Mathematical Object Manager) to locate and retrieve
183 mathematical items from the \helm{} library.
184 The proof status that are exchanged
185 by the \hbugs{} actors, instead, are built on the fly and are neither
186 stored nor given an unique identifier (URI) to be managed by the
190 \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
191 {\hbugs{} \wss{} interfaces}
193 Brokers are the key actors of the \hbugs{} architecture since they
194 act as intermediaries between clients and tutors. They behave as \wss{}
195 providers and requesters for \emph{both} clients and tutors, see Fig.
198 With respect to the client, a broker acts as a \ws{} provider, receiving the
199 proof status and forwarding it to one or more tutors.
200 It also acts as a \ws{} requester sending
201 hints to the client as soon as they are available from the tutors.
203 With respect to the tutors, the \ws{} provider role is accomplished by
204 receiving hints as soon as they are produced; as a requester, it is
205 accomplished by asking for computations (\emph{musings} in \hbugs{}
206 terminology) on status received by clients and by stopping already late but
207 still ongoing \musings{}.
209 Additionally brokers keep track of available tutors and clients
212 \hbugs{} brokers act as MONET brokers implementing the following components:
213 Client Manager, Service Registry Manager (keeping track of available
214 tutors), Planning Manager (choosing the available tutors among the ones to
215 which the client is subscribed), Execution Manager. The Service Manager
216 component is not required since the session handler, that identifies
217 a session between a service and a broker, is provided to the service by
218 the broker instead of being received from the service when the session is
219 initialized. In particular, a session is identified by an unique identifier
220 for the client (its URL) and an unique identifier for the broker (its
223 Notice that \hbugs{} brokers have no knowledge of the domain area of
224 proof-assistants, nor they are able to interpret the messages that they
225 are forwarding. They are indeed only in charge of maintaining the
226 abstraction of several reasoning blackboards --- one for each client ---
227 of capacity one: a blackboard is created when the client submits a problem;
228 it is then ``shared'' by the client and all the tutors until the client
229 submits a new problem. Replacing the client with a CAS and all the tutors
230 with agents implementing different resolution methods for differential
231 equations would not require any change in the broker. Notice, however,
232 that all the tutors must expose the same interface to the broker.
234 The MONET architecture specification does not state explicitly whether
235 the service and broker answers can be asynchronous. Nevertheless, the
236 described information flow implicitly suggests a synchronous implementation.
237 On the contrary, in \hbugs{} every request is asynchronous: the connection
238 used by an actor to issue a query is immediately closed; when a service
239 produces an answer, it gives it back to the issuer by calling the
240 appropriate actor's method.
243 Tutors are software components able to consume proof status producing hints.
244 \hbugs{} does not specify by which means hints should be produced: tutors
245 can use any means necessary (heuristics, external theorem prover or CAS,
246 etc.). The only requirement is that there exists an agreement on the formats
247 of proof status and hints.
249 Tutors act both as \ws{} providers and requesters for the broker, see Fig.
251 providers, they wait for commands requesting to start a new \musing{} on
252 a given proof status or to stop an old, out of date, \musing{}. As
253 requesters, they signal to the broker the end of a \musing{} along with its
254 outcome (a hint in case of success or a failure notification).
256 \hbugs{} tutors act as MONET services.
258 \section{An \hbugs{} Session Example}
260 In this section we describe a typical \hbugs{} session. The aim of the
261 session is to solve the following easy exercise:
263 Let $x$ be a generic real number. Using the \helm{} proof-engine,
266 x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
270 Let us suppose that the \hbugs{} broker is already running and that the
271 tutors already registered themselves to the broker.
272 When the user starts \texttt{gTopLevel}, the system registers itself to
273 the broker, that sends back the list of available tutors. By default,
274 \texttt{gTopLevel} notifies to the broker its intention of subscribing to every
275 tutor available. The user can always open a configuration window where she
276 is presented the list of available tutors and she can independently subscribe
277 and unsubscribe the system to each tutor.
279 \myincludegraphics{step1}{t}{12cm}{Example session.}
281 %\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
282 % {Example session, snapshot 2.}
284 The user can now insert into the system the statement of the theorem and start
285 proving it. Let us suppose that the first step of the user is proving
286 that the denominator 2 is different from 0. Once that this technical result
287 is proven, the user must prove the goal shown in the upper right corner
288 of the window in background in Fig. \ref{step1}.
290 While the user is wondering how to proceed in the proof, the tutors are
291 trying to progress in the proof. After a while, the tutors' suggestions
292 start to appear in the lower part of the \hbugs{} interface window
293 (the topmost window in Fig. \ref{step1}). In this case, the tutors are able
294 to produce 23 hints. The first and not very useful hint suggests to proceed in
295 the proof by exchanging the two sides of the equality.
296 The second hint suggests to reduce both sides of the equality to their normal
297 form by using only reductions which are justified by the ring structure of the
298 real numbers; the two normal forms, though, are so different that the proof is
299 not really simplified.
300 All the residual 21 hints suggest to apply one lemma from the distributed
301 library of \helm{}. The user can look at the statement of the lemma by clicking
304 The user can now look at the list of suggestions and realize that a good one is
305 applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
306 members by the same scalar\footnote{Even if she does not receive the hint, the
307 user probably already knows that this is the right way to proceed. The
308 difficult part where the hint helps is guessing what is the name of the lemma
310 Double-clicking on the hint automatically applies
311 the lemma, reducing the proof to closing three new goals. The first one asks
312 the user the scalar to use as an argument of the previous lemma; the second
313 one states that the scalar is different from 0; the third lemma (the main
314 one) asks to prove the equality between the two new members.
315 % is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
316 % the still unknown scalar argument, which can have only $H$ and $x$ as
319 The user proceeds by instantiating the scalar with the number 2. The
320 \texttt{Assumption} tutor now suggests to close the second goal (that
321 states that $2 \neq 0$) by applying the hypothesis $H$.
322 No useful suggestions, instead, are generated for the main goal
323 $2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
324 To proceed in the proof the user needs to simplify the
325 expression using the lemma $Rinv\_r\_simpl\_m$ that states that
326 $\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
327 suggesting simplifications, the user must find out this simplification by
328 himself. Once she founds it, the goal is reduced to proving that
329 $2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
330 \texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is
331 just one of the 22 hints that the user receives. It is the only hint that
332 does not open new goals, but the user right now does not have any way to know
333 that.} to the user how to directly finish the proof.
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
336 % Comandi da dare a gTopLevel %
337 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
339 % !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
343 % Simpl (per fare unfold di Rdiv)
345 % (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
347 % (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
349 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
351 \section{Implementation's Highlights}
352 \label{implementation}
353 In this section we present some of the most relevant implementation details of
354 the \hbugs{} architecture.
357 \paragraph{Proof status}
358 In our implementation of the \hbugs{} architecture we used the proof
359 assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
360 client. Thus we have implemented serialization/deserialization capabilities
361 for its internal status. In order to be able to describe \wss{} that
362 exchange status in WSDL using the XML Schema type system, we have chosen an
363 XML format as the target format for the serialization.
365 % A schematic representation of the gTopLevel internal status is depicted in
367 Each proof is represented by a tuple of four elements:
368 \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
370 % \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
374 \item[uri]: an URI chosen by the user at the beginning of the proof
375 process. Once (and if) proved, that URI will globally identify the term
376 inside the \helm{} library (given that the user decides to save it).
377 \item[thesis]: the ongoing proof thesis
378 \item[proof]: the current incomplete proof tree. It can contain
379 \emph{metavariables} (holes) that stands for the parts of the proof
380 that are still to be completed. Each metavariable appearing in the
381 tree references one element of the metavariables environment
383 \item[metasenv]: the metavariables environment is a list of
384 \emph{goals} (unproved conjectures).
385 In order to complete the proof, the user has to instantiate every
386 metavariable in the proof with a proof of the corresponding goal.
387 Each goal is identified by an unique identifier and has a context
388 and a type (the goal thesis). The context is a list of named
389 hypotheses (declarations and definitions). Thus the context and the goal
390 thesis form a sequent, which is the statement of the proof that will
391 be used to instantiate the metavariable occurrences.
394 Each of these information is represented in XML as described in
395 \cite{mowglicic}. Additionally, an \hbugs{} status carries the unique
396 identifier of the current goal, which is the goal the user is currently
397 focused on. Using this value it is possible to implement different client
398 side strategies: the user could ask the tutors to work on the goal
399 she is considering or to work on the other ``background'' goals.
402 A hint in the \hbugs{} architecture should carry enough information to
403 permit the client to progress in the current proof. In our
404 implementation each hint corresponds to either one of the tactics available
405 to the user in gTopLevel (together with its actual arguments) or a set
406 of alternative suggestions (a list of hints).
408 For tactics that don't require any particular argument (like tactics that
409 apply type constructors or decision procedures)
410 only the tactic name is represented in the hint. For tactics that need
411 terms as arguments (for example the \texttt{Apply} tactic that apply a
412 given lemma) the hint includes a textual representation of them, using the
413 same representation used by the interactive proof assistant when querying
414 user for terms. In order to be transmitted between \wss{}, hints are
417 It is also possible for a tutor to return more hints at once,
418 grouping them in a particular XML element.
419 This feature turns out to be particularly useful for the
420 \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that
421 queries a lemma database and returns to the client a list of all lemmas that
422 could be used to complete the proof. This particular hint is encoded as a
423 list of \texttt{Apply} hints, each of them having one of the results as term
426 We would like to stress that the \hbugs{} architecture has no dependency
427 on either the hint or the status representation: the only message parts
428 that are fixed are those representing the administrative messages
429 (the envelopes in the \wss{} terminology). In particular, the broker can
430 manage at the same time several sessions working on different status/hints
431 formats. Of course, there must be an agreement between the clients
432 and the tutors on the format of the data exchanged.
434 In our implementation the client does not trust the tutors hints:
435 being encoded as references to available tactics imply
436 that an \hbugs{} client, upon receival of a hint, simply try to replay
438 done by a tutor on the local copy of the proof. The application of the hint
439 can even fail to type check and the client copy of the proof can be left
440 undamaged after spotting the error. Note, however, that it is still
441 possible to implement a complex tutor that looks for a proof doing
443 send back to the client a hint whose argument is a witness (a trace) of
444 the proof found: the client applies the hint reconstructing (and checking
445 the correctness of) the proof from the witness, without having to
446 re-discover the proof itself.
448 An alternative implementation where the tutors are trusted would simply
449 send back to the client a new proof-status. Upon receiving the
450 proof-status, the client would just override its current proof status with
451 the suggested one. In the case of those clients which are implemented
452 using proof-objects (as the Coq proof-assistant, for instance), it is
453 still possible for the client to type-check the proof-object and reject
454 wrong hints. The systems that are not based on proof-objects
455 (as PVS, NuPRL, etc.), instead, have to trust the new proof-status. In this
456 case the \hbugs{} architecture needs at least to be extended with
457 clients-tutors authentication.
459 \paragraph{Registries}
460 Being central in the \hbugs{} architecture, the broker is also responsible
461 of housekeeping operations both for clients and tutors. These operations are
462 implemented using three different data structures called \emph{registries}:
463 clients registry, tutors registry and \musings{} registry.
465 In order to use the suggestion engine a client should register itself to the
466 broker and subscribe to one or more tutors. The registration phase is
467 triggered by the client using the \texttt{Register\_client} method of the
468 broker to send him an unique identifier and its base URI as a
469 \ws{}. After the registration, the client can use broker's
470 \texttt{List\_tutors} method to get a list of available tutors.
471 Eventually the client can subscribe to one or more of these using broker's
472 \texttt{Subscribe} method. Clients can also unregister from brokers using
473 \texttt{Unregister\_client} method.
475 The broker keeps track of both registered clients and clients' subscriptions
476 in the clients registry.
478 In order to be advertised to clients during the subscription phase, tutors
479 should register to the broker using the broker's \texttt{Register\_tutor}
480 method. This method is really similar to \texttt{Register\_client}:
481 tutors are required to send an unique identifier and a base URI for their
483 Additionally tutors are required to send an human readable description of
484 their capabilities; this information could be used by client's user to
485 decide which tutors he wants to subscribe to. As the clients, tutors can
486 unregister from brokers using \texttt{Unregister\_broker} method.
488 Each time the client status changes, it get sent sent to the
489 broker using its \texttt{Status} method. Using both clients registry (to
490 lookup client's subscription) and tutors registry (to check if some tutors
491 has unsubscribed), the broker is able to decide to which tutors the
492 new status have to be forwarded.
493 % \ednote{CSC: qui o nei lavori futuri parlare
494 % della possibilit\'a di avere un vero brocker che multiplexi le richieste
495 % dei client localizzando i servizi, etc.}
497 The forwarding operation is performed using the \texttt{Start\_musing}
498 method of the tutors, that is a request to start a new computation
499 (\emph{\musing{}}) on a given status. The return value of
500 \texttt{Start\_musing} is a
501 \musing{} identifier that is saved in the \musings{} registry along with
502 the identifier of the client that triggered the \musing{}.
504 As soon as a tutor completes an \musing{}, it informs the broker
505 using its \texttt{Musing\_completed} method; the broker can now remove the
506 \musing{} entry from the \musings{} registry and, depending on its outcome,
507 inform the client. In case of success one of the \texttt{Musing\_completed}
508 arguments is a hint to be sent to the client, otherwise there's no need to
509 inform him and the \texttt{Musing\_completed} method is called
510 just to update the \musings{} registry.
512 Consulting the \musings{} registry, the broker is able to know, at each
513 time, which \musings{} are in execution on which tutor. This peculiarity is
514 exploited by the broker on invocation of the \texttt{Status} method.
515 Receiving a new status from the client implies indeed that the previous
516 status no longer exists and all \musings{} working on it should be stopped:
517 additionally to the already described behavior (i.e. starting new
518 \musings{} on the received status), the broker takes also care of stopping
519 ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
522 As already discussed, all \hbugs{} actors act as \wss{} offering one or more
523 services to neighbor actors. To grant as most accessibility as possible to
524 our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given
525 that our proof assistant was entirely developed in the Objective Caml
526 language, we have chosen to develop also \hbugs{} in that language in order
527 to maximize code reuse. To develop \wss{} in Objective Caml we have
528 developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
529 write HTTP 1.1 Web servers and abstract over GET/POST parsing. This library
530 supports different kinds of Web servers architectures, including
531 multi-process and multi-threaded ones.} bindings described in
535 Each tutor exposes a \ws{} interface and should be able to work, not only for
536 many different clients referring to a common broker, but also for many
537 different brokers. The potential high number of concurrent clients imposes
538 a multi-threaded or multi-process architecture.
540 Our current implementation is based on a multi threaded architecture
541 exploiting the capabilities of the O'HTTP library \cite{zack}. Each tutor is
542 composed by one thread always running plus
543 an additional thread for each running \musing{}. One thread is devoted to
544 listening for incoming \ws{} request; upon correct receiving requests it
545 pass the control to a second thread, created on the fly, to handle the
546 incoming request following the classical one-thread-per-request approach in
548 If the received request is \texttt{Start\_musing}, a new thread is
549 spawned to handle it; the thread in duty to handle the HTTP request
550 returns an HTTP response containing the identifier of the just started
551 \texttt{musing}, and then dies. If the received request is
552 \texttt{Stop\_musing}, instead, the spawned thread kills the thread
553 responsible for the \texttt{musing} whose identifier is the argument
554 of the \texttt{Stop\_musing} method.
556 This architecture turns out to be scalable and allows the running threads
557 to share the cache of loaded (and type-checked) theorems.
558 As we will explain in Sect. \ref{tutors}, this feature turns out to be
559 really useful for tactics that rely on a huge but fixed set of lemmas,
560 as every reflexive tactic.
562 The implementation of a tutor within the described architecture is not that
563 difficult having a language with good threading capabilities (as OCaml has)
564 and a pool of already implemented tactics (as gTopLevel has).
565 Still working with threads is known to be really error prone due to
566 concurrent programming intrinsic complexity. Moreover, there is a
567 non-neglectable part of code that needs to be duplicated in every tutor:
568 the code to register the tutor to the broker and to handle HTTP requests;
569 the code to manage the creation and termination of threads; and the code for
570 parsing the requests and serializing the answers. As a consequence we
571 have written a generic implementation of a tutor which is parameterized
572 over the code that actually propose the hint and some administrative
573 data (as the port the tutor will be listening to).
575 The generic tutor skeleton is really helpful in writing new tutors.
576 Nevertheless, the code obtained by converting existing tactics into tutors
577 is still quite repetitive: every tutor that wraps a tactic has to
578 instantiate its own copy of the proof-engine kernel and, for each request,
579 it has to override its status, guess the tactic arguments, apply the tactic
580 and, in case of success, send back a hint with the tactic name and the
581 chosen arguments. Of course, the complex part of the work is guessing the
582 right arguments. For the simple case of tactics that do not require
583 any argument, though, we are able to automatically generate the whole
584 tutor code given the tactic name. Concretely, we have written a
585 tactic-based tutor template and a script that parses an XML file with
586 the specification of the tutor and generates the tutor's code.
587 The XML file describes the tutor's port, the code to invoke the tactic,
588 the hint that is sent back upon successful application and a
589 human readable explanation of the tactic implemented by the tutor.
591 \section{The Implemented \hbugs Tutors}
593 To test the \hbugs{} architecture and to assess the utility of a suggestion
594 engine for the end user, we have implemented several tutors. In particular,
595 we have investigated three classes of tutors:
597 \item \emph{Tutors for beginners}. These are tutors that implement tactics
598 which are neither computationally expensive nor difficult to understand:
599 an expert user can always understand if the tactic can be applied or not
600 without having to try it. For example, the following implemented tutors
601 belong to this class:
603 \item \emph{Assumption Tutor}: it ends the proof if the thesis is
604 equivalent\footnote{In our implementation, the equivalence relation
605 imposed by the logical framework is \emph{convertibility}. Two
606 expressions are convertible when they reduce to the same normal form.
607 Two ``equal'' terms depending on free variables can be non-convertible
608 since free variables stop the reduction. For example, $2x$ is convertible
609 with $(3-1)x$ because they both reduce to the same normal form
610 $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
611 already in normal form.}
612 to one of the hypotheses\footnote{
613 In some cases, especially when non-trivial computations are involved,
614 the user is totally unable to figure out the convertibility of two terms.
615 In these cases the tutor becomes handy also for expert users.}.
616 \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
617 adsurdum} if one hypothesis is equivalent to $False$.
618 \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
619 suggests to apply the commutative property.
620 \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
621 the Constructor Tutor suggests to proceed in the proof by applying one
622 or more constructors when the goal thesis is an inductive type or a
623 proposition inductively defined according to the declarative
624 style\footnote{An example of a proposition that can be given in
625 declarative style is the $\le$ relation over natural numbers:
626 $\le$ is the smallest relation
627 such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
628 that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
629 of $n \le n$ is simply the application of the first constructor to
630 $n$ and a proof of $n \le m$ is the application of the second
631 constructor to $n,m$ and a proof of $n \le m$.}.
632 Since disjunction, conjunction, existential quantification and
633 Leibniz equality are particular cases of inductive propositions,
634 all the other tutors of this class are instantiations of the
635 the Constructor tactic. Left and Right suggest to prove a disjunction
636 by proving its left/right member; Split reduces the proof of a
637 conjunction to the two proof of its members; Exists suggests to
638 prove an existential quantification by providing a
639 witness\footnote{This task is left to the user.}; Reflexivity proves
640 an equality whenever the two sides are convertible.
642 Beginners, when first faced with a tactic-based proof-assistant, get
643 lost quite soon since the set of tactics is large and their names and
644 semantics must be remembered by heart. Tutorials are provided to guide
645 the user step-by-step in a few proofs, suggesting the tactics that must
646 be used. We believe that our beginners tutors can provide an auxiliary
647 learning tool: after the tutorial, the user is not suddenly left alone
648 with the system, but she can experiment with variations of the proof given
649 in the tutorial as much as she like, still getting useful suggestions.
650 Thus the user is allowed to focus on learning how to do a formal proof
651 instead of wasting efforts trying to remember the interface to the system.
652 \item \emph{Tutors for Computationally Expensive Tactics}. Several tactics have
653 an unpredictable behavior, in the sense that it is unfeasible to understand
654 whether they will succeed or they will fail when applied and what will be
655 their result. Among them, there are several tactics either computationally
656 expensive or resource consuming. In the first case, the user is not
657 willing to try a tactic and wait for a long time just to understand its
658 outcome: she would prefer to keep on concentrating on the proof and
659 have the tactic applied in background and receive out-of-band notification
660 of its success. The second case is similar, but the tactic application must
661 be performed on a remote machine to avoid overloading the user host
662 with several concurrent resource consuming applications.
664 Finally, several complex tactics and in particular all the tactics based
665 on reflexive techniques depend on a pretty large set of definitions, lemmas
666 and theorems. When these tactics are applied, the system needs to retrieve
667 and load all the lemmas. Pre-loading all the material needed by every
668 tactic can quickly lead to long initialization times and to large memory
669 footstamps. A specialized tutor running on a remote machine, instead,
670 can easily pre-load the required theorems.
672 As an example of computationally expensive task, we have implemented
673 a tutor for the \emph{Ring} tactic \cite{ringboutin}.
674 The tutor is able to prove an equality over a ring by reducing both members
675 to a common normal form. The reduction, which may require some time in
677 is based on the usual commutative, associative and neutral element properties
678 of a ring. The tactic is implemented using a reflexive technique, which
679 means that the reduction trace is not stored in the proof-object itself:
680 the type-checker is able to perform the reduction on-the-fly thanks to
681 the conversion rules of the system. As a consequence, in the library there
682 must be stored both the algorithm used for the reduction and the proof of
683 correctness of the algorithm, based on the ring axioms. This big proof
684 and all of its lemmas must be retrieved and loaded in order to apply the
685 tactic. The Ring tutor loads and caches all the required theorems the
686 first time it is contacted.
687 \item \emph{Intelligent Tutors}. Expert users can already benefit from the previous
688 class of tutors. Nevertheless, to achieve a significative production gain,
689 they need more intelligent tutors implementing domain-specific theorem
690 provers or able to perform complex computations. These tutors are not just
691 plain implementations of tactics or decision procedures, but can be
692 more complex software agents interacting with third-parties software,
693 such as proof-planners, CAS or theorem-provers.
695 To test the productivity impact of intelligent tutors, we have implemented
696 a tutor that is interfaced with the \helm{}
697 Search-Engine\footnote{\url{http://helm.cs.unibo.it/library.html}} and that
698 is able to look for every theorem in the distributed library that can
699 be applied to proceed in the proof. Even if the tutor deductive power
700 is extremely limited\footnote{We do not attempt to check if the new goals
701 obtained applying a lemma can be automatically proved or, even better,
702 automatically disproved to reject the lemma.}, it is not unusual for
703 the tutor to come up with precious hints that can save several minutes of
704 work that would be spent in proving again already proven results or
705 figuring out where the lemmas could have been stored in the library.
708 \section{Conclusions and Future Work}
710 In this paper we described a suggestion engine architecture for
711 proof-assistants: the client (a proof-assistant) sends the current proof
712 status to several distributed \wss{} (called tutors) that try to progress
713 in the proof and, in case of success, send back an appropriate hint
714 (a proof-plan) to the user. The user, that in the meantime was able to
715 reason and progress in the proof, is notified with the hints and can decide
716 to apply or ignore them. A broker is provided to decouple the clients and
717 the tutors and to allow the client to locate and invoke the available remote
718 services. The whole architecture is an instance of the MONET architecture
719 for Mathematical \wss{}.
721 A running prototype has been implemented as part of the
722 \helm{} project \cite{helm}
723 and we already provide several tutors. Some of them are simple tutors that
724 try to apply one or more tactics of the \helm{} Proof-Engine, which is also
725 our client. We also have a much more complex tutor that is interfaced
726 with the \helm{} Search-Engine and looks for lemmas that can be directly
729 Future works comprise the implementation of new features and tutors, and
730 the embedding of the system in larger test cases. For instance, one
731 interesting case study would be interfacing a CAS as Maple to the
732 \hbugs{} broker, developing at the same time a tutor that implements the
733 Field tactic of Coq, which proves the equality of two expressions in an
734 abstract field by reducing both members to the same normal form. CAS can
735 produce several compact normal forms, which are particularly informative
736 to the user and help in proceeding in a proof. Unfortunately, CAS do not
737 provide any certificate about the correctness of the simplification. On
738 the contrary, the Field tactic certifies the equality of two expressions,
739 but produces normal forms that are hardly a simplification of the original
740 formula. The benefits for the CAS would be obtained by using the Field tutor
741 to certify the CAS simplifications, proving that the Field normal form
742 of an expression is preserved by the simplification.
743 More advanced tutors could exploit the CAS to reduce the
744 goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
745 certify the simplification according to the skeptical approach.
747 We have many plans for further developing both the \hbugs{} architecture and
748 our prototype. Interesting results could be obtained
749 augmenting the informative content of each suggestion. We can for example
750 modify the broker so that also negative results are sent back to the client.
751 Those negative suggestions could be reflected in the user interface by
752 deactivating commands to narrow the choice of tactics available to the user.
753 This approach could be interesting especially for novice users, but requires
754 the client to trust other actors a bit more than in the current approach.
756 We plan also to add some rating mechanism to the architecture. A first
757 improvement in this direction could be distinguishing between hints that, when
758 applied, are able to completely close one or more goals and
759 tactics that progress in the proof by reducing one or more goals to new goals:
760 the new goals could be false and the proof can be closed only by backtracking.
762 Other heuristics and/or measures could be added to rate
763 hints and show them to the user in a particular order: an interesting one
764 could be a measure that try to minimize the size of the generated proof,
765 privileging therefore non-overkilling solutions \cite{ring}.
767 We are also considering to follow the \OmegaAnts{} path more closely adding
768 ``recursion'' to the system so that the proof status resulting from the
769 application of old hints are cached somewhere and could be used as a starting
770 point for new hint searches. The approach is interesting, but it represents
771 a big shift towards automatic theorem proving: thus we must consider if it is
772 worth the effort given the increasing availability of automation in proof
773 assistants tactics and the ongoing development of \wss{} based on
774 already existent and well developed theorem provers.
776 Even if not strictly part of the \hbugs{} architecture, the graphical user
777 interface (GUI) of our prototype needs a lot of improvement if we would like
778 it to be really usable by novices. In particular, the user is too easily
779 distracted by the tutor's hints that are ``pushed'' to her.
781 Our \wss{} still lack a real integration in the MONET architecture,
782 since we do not provide the different ontologies to describe our problems,
783 solutions, queries, and services. In the short term, completing this task
784 could provide a significative feedback to the MONET consortium and would
785 enlarge the current set of available MONET actors on the Web. In the long
786 term, new more intelligent tutors could be developed on top of already
787 existent MONET \wss{}.
789 To conclude, \hbugs{} is a nice experiment meant to understand whether the
790 current \wss{} technology is mature enough to have a concrete and useful
791 impact on the daily work of proof-assistants users. So far, only the tutor
792 that is interfaced with the \helm{} Search-Engine has effectively increased
793 the productivity of experts users. The usefulness of the tutors developed for
794 beginners, instead, need further assessment.
796 \begin{thebibliography}{01}
798 \bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
799 \url{http://www.w3.org/TR/2003/WD-ws-gloss-20030514/}
801 \bibitem{wsdlbindings} Web Services Description Language (WSDL)
802 Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
803 \url{http://www.w3.org/TR/wsdl12-bindings/}
805 \bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
806 Deduction Systems via the Logic Broker Architecture. In Proceedings
807 of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
809 \bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
810 the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
813 \bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
814 Mathematical Knowledge Management in HELM. In Annals of Mathematics and
815 Artificial Intelligence, 38(1): 27--46, May 2003.
817 \bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
818 at Combining Interactive and Automated Theorem Proving. In M. Kerber and
819 M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
822 \bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
823 Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
824 Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
826 \bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler,
827 X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier,
828 W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical
829 Assistant. In W. McCune (ed), Proceedings of the 14th Conference on
830 Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255,
831 Townsville, Australia, 1997.
833 \bibitem{ringboutin} S. Boutin. Using reflection to build efficient and
834 certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
835 TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
837 \bibitem{maplemodeforCoq} David Delahaye, Micaela Mayero.
838 A Maple Mode for Coq. Contribution to the Coq library.\\
839 \url{htpp://coq.inria.fr/contribs/MapleMode.html}
841 \bibitem{MONET-Overview} The MONET Consortium, MONET Architecture Overview,
842 Public Deliverable D04 of the MONET Project.\\
843 \url{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
845 \bibitem{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable
847 \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html}
849 \bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the
850 Bad Habit of Overkilling. In Supplementary Proceedings of the 14th
851 International Conference TPHOLS 2001, pp. 352--367, Edinburgh.
853 \bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
854 dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
856 \bibitem{ws3} J. Zimmer and M. Kohlhase. System Description: The MathWeb
857 Software Bus for Distributed Mathematical Reasoning.
858 In Proceedings of the 18th International Conference on Automated Deduction
859 CADE 18, LNAI 2392, Springer Verlag, 2002.
861 \bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
862 Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
864 \end{thebibliography}