X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Fhbugs-calculemus-2003.tex;fp=helm%2Fpapers%2Fcalculemus-2003%2Fhbugs-calculemus-2003.tex;h=0000000000000000000000000000000000000000;hp=431fbb9b716186c01bbf51f162fc02f9c74653c3;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex deleted file mode 100644 index 431fbb9b7..000000000 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ /dev/null @@ -1,873 +0,0 @@ -\documentclass[runningheads]{llncs} -\pagestyle{headings} -\setcounter{page}{1} -\usepackage{graphicx} -\usepackage{amsfonts} - -% \myincludegraphics{filename}{place}{width}{caption}{label} -\newcommand{\myincludegraphics}[5]{ - \begin{figure}[#2] - \begin{center} - \includegraphics[width=#3]{eps/#1.eps} - \caption[#4]{#5} - \label{#1} - \end{center} - \end{figure} -} - -%\usepackage[show]{ed} -%\usepackage{draftstamp} - -\newcommand{\musing}{\texttt{musing}} -\newcommand{\musings}{\texttt{musings}} -\newcommand{\ws}{Web-Service} -\newcommand{\wss}{Web-Services} -\newcommand{\hbugs}{H-Bugs} -\newcommand{\helm}{HELM} -\newcommand{\Omegapp}{$\Omega$mega} -\newcommand{\OmegaAnts}{$\Omega$mega-Ants} - -\title{Brokers and Web-Services for Automatic Deduction: a Case Study} - -\author{ - Claudio Sacerdoti Coen\thanks{Partially supported by `MoWGLI: Math on the Web, Get it by Logic and Interfaces', EU IST-2001-33562} \and - Stefano Zacchiroli\thanks{Partially supported by `MyThS: Models and Types for Security in Mobile Distributed Systems', EU FET-GC IST-2001-32617}} - -\institute{ - Department of Computer Science\\ - University of Bologna\\ - Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\ - \email{sacerdot@cs.unibo.it} - \and - Department of Computer Science\\ - \'Ecole Normale Sup\'erieure\\ - 45, Rue d'Ulm, F-75230 Paris Cedex 05, FRANCE\\ - \email{zack@cs.unibo.it} -} - -\date{ } - -\begin{document} -\sloppy -\maketitle - -\begin{abstract} - We present a planning broker and several Web-Services for automatic deduction. - Each Web-Service implements one of the tactics usually available in - interactive proof-assistants. When the broker is submitted a ``proof status'' - (an incomplete proof tree and a focus on an open goal) it dispatches the proof - to the Web-Services, collects the successful results, and send them back to - the client as ``hints'' as soon as they are available. - - In our experience this architecture turns out to be helpful both for - experienced users (who can take benefit of distributing heavy computations) - and beginners (who can learn from it). -\end{abstract} - -\section{Introduction} - The \ws{} approach at software development seems to be a working solution for - getting rid of a wide range of incompatibilities between communicating - software applications. W3C's efforts in standardizing related technologies - grant longevity and implementations availability for frameworks based on - \wss{} for information exchange. As a direct consequence, the number of such - frameworks is increasing and the World Wide Web is moving from a disorganized - repository of human-understandable HTML documents to a disorganized repository - of applications working on machine-understandable XML documents both for input - and output. - - The big challenge for the next future is to provide stable and reliable - services over this disorganized, unreliable, and ever-evolving architecture. - The standard solution is to provide a further level of stable services (called - \emph{brokers}) that behave as common gateways/addresses for client - applications to access a wide variety of services and abstract over them. - - Since the \emph{Declaration of Linz}, the MONET - Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}} - is working on the development of a framework, based on the - \wss{}/brokers approach, aimed at providing a set of software tools for the - advertisement and the discovery of mathematical \wss{}. - %CSC This framework turns out to be strongly based on both \wss{} and brokers. - - Several groups have already developed software bus and - services\footnote{The most part of these systems predate the development of - \wss. Those systems whose development is still active are slowly being - reimplemented as \wss.} providing both computational and reasoning - capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of - Computer Algebra Systems; the second ones provide interfaces to well-known - theorem provers. - Proof-planners, proof-assistants, CASs and - domain-specific problem solvers are natural candidates to be clients of these - services. Nevertheless, so far the number of examples in the literature has - been insufficient to fully assess the concrete benefits of the framework. - - In this paper we present an architecture, namely \hbugs{}, implementing a - \emph{suggestion engine} for the proof assistant developed on behalf of the - \helm{}\footnote{Hypertextual Electronic Library of Mathematics, - \url{http://helm.cs.unibo.it}} project - \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to - suggest possible ways to proceed in a proof. The tutors are orchestrated - by a broker (a \ws{} itself) that is able to dispatch a proof - status from a client (the proof-assistant) to the tutors; - each tutor tries to make progress in the proof and, in case - of success, notifies the client that shows an \emph{hint} to the user. - The broker is an instance of the homonymous entity of the MONET framework. - The tutors are MONET services. Another \ws{} (which is not described in this - paper and which is called Getter \cite{zack}) is used to locate and download - mathematical entities; the Getter plays the role of the Mathematical Object - Manager of the MONET framework. - - A precursor of \hbugs{} is the \OmegaAnts{} project - \cite{omegaants1,omegaants2}, which provided similar functionalities to the - \Omegapp{} proof-planner \cite{omega}. The main architectural difference - between \hbugs{} and \OmegaAnts{} is that the latter is based on a - black-board architecture and it is not implemented using \wss{} and - brokers. - - In Sect. \ref{architecture} we present the architecture of \hbugs{}. - A usage session is shown in Sect. \ref{usage}. - Further implementation details are given in Sect. \ref{implementation}. - Sect. \ref{tutors} is an overview of the tutors that have been implemented. - As usual, the final section of this paper is devoted to conclusions and future works. - -\section{An \hbugs{} Bird's Eye View} -\label{architecture} - \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture} - - The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three - different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}. - Each actor presents one or more \ws{} interfaces to its neighbors \hbugs{} - actors. - - In this section we detail the role and requirements of each kind of - actors and we discuss about the correspondences between them and the MONET - entities described in \cite{MONET-Overview}. - Due to lack of space, we cannot compare our framework to similar proposals, as - the older and more advanced \Omegapp{} system. The study of the - correspondences with MONET is well motivated by the fact that the MONET - framework is still under development and that our implementation is one of the - first experiments in \ws based distributed reasoning. On the other hand, a - comparison with \Omegapp{} would be less interesting since the functionalities we - provide so far are just a subset of the \OmegaAnts{} ones. - - \paragraph{Clients} - An \hbugs{} client is a software component able to produce \emph{proof - status} and to consume \emph{hints}. - - A proof status is a representation of an incomplete proof and is supposed to - be informative enough to be used by an interactive proof assistant. No - additional requirements exist on the proof status, but there should be an - agreement on its format between clients and tutors. A hint is an - encoding of a step that can be performed in order to proceed in an - incomplete proof. Usually it represents a reference to a tactic available - on some proof assistant along with an instantiation for its formal - parameters. Hints can also be more structured: a hint can be - as complex as a whole proof-plan. - - Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{} - providers and requesters, see Fig. \ref{interfaces}. - They act as providers receiving hints from the broker; they act as - requesters submitting new status to the tutors. - Clients additionally use broker services to know which tutors are available - and to subscribe to one or more of them. - - Usually, when the client role is taken by an interactive proof assistant, - new status are sent to the broker as soon as the proof change (e.g. when the - user applies a tactic or when a new proof is started); hints are shown to - the user by the means of some effects in the user interface (e.g. popping a - dialog box or enlightening a tactic button). - - \hbugs{} clients act as MONET clients and ask brokers to provide access to a - set of services (the tutors). \hbugs{} has no actors corresponding to - MONET's Broker Locating Service (since the client is supposed to know the - URI of at least one broker). The \hbugs{} clients and tutors contact the - Getter (a MONET Mathematical Object Manager) to locate and retrieve - mathematical items from the \helm{} library. - The proof status that are exchanged - by the \hbugs{} actors, instead, are built on the fly and are neither - stored nor given an unique identifier (URI) to be managed by the - Getter. - - \paragraph{Brokers} - \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces} - {\hbugs{} \wss{} interfaces} - - Brokers are the key actors of the \hbugs{} architecture since they - act as intermediaries between clients and tutors. They behave as \wss{} - providers and requesters for \emph{both} clients and tutors, see Fig. - \ref{interfaces}. - - With respect to the client, a broker acts as a \ws{} provider, receiving the - proof status and forwarding it to one or more tutors. - It also acts as a \ws{} requester sending - hints to the client as soon as they are available from the tutors. - - With respect to the tutors, the \ws{} provider role is accomplished by - receiving hints as soon as they are produced; as a requester, it is - accomplished by asking for computations (\emph{musings} in \hbugs{} - terminology) on status received by clients and by stopping already late but - still ongoing \musings{}. - - Additionally brokers keep track of available tutors and clients - subscriptions. - - \hbugs{} brokers act as MONET brokers implementing the following components: - Client Manager, Service Registry Manager (keeping track of available - tutors), Planning Manager (choosing the available tutors among the ones to - which the client is subscribed), Execution Manager. The Service Manager - component is not required since the session handler, that identifies - a session between a service and a broker, is provided to the service by - the broker instead of being received from the service when the session is - initialized. In particular, a session is identified by an unique identifier - for the client (its URL) and an unique identifier for the broker (its - URL). - - Notice that \hbugs{} brokers have no knowledge of the domain area of - proof-assistants, nor they are able to interpret the messages that they - are forwarding. They are indeed only in charge of maintaining the - abstraction of several reasoning blackboards --- one for each client --- - of capacity one: a blackboard is created when the client submits a problem; - it is then ``shared'' by the client and all the tutors until the client - submits the next problem. For instance, replacing the client with a CAS and - all the tutors with agents implementing different resolution methods for - differential equations would not require any change in the broker. Notice - that all the tutors must expose the same interface to the broker. - - The MONET architecture specification does not state explicitly whether the - service and broker answers can be asynchronous. Nevertheless, the - described information flow implicitly suggests a synchronous implementation. - On the contrary, in \hbugs{} every request is asynchronous: the connection - used by an actor to issue a query is immediately closed; when a service - produces an answer, it gives it back to the issuer by calling the - appropriate actor's method. - - \paragraph{Tutors} - Tutors are software components able to consume proof status producing hints. - \hbugs{} does not specify by which means hints should be produced: tutors - can use any means necessary (heuristics, external theorem prover or CAS, - etc.). The only requirement is that there exists an agreement on the formats - of proof status and hints. - - Tutors act both as \ws{} providers and requesters for the broker, see Fig. - \ref{interfaces}. As - providers, they wait for commands requesting to start a new \musing{} on - a given proof status or to stop an old, out of date, \musing{}. As - requesters, they signal to the broker the end of a \musing{} along with its - outcome (a hint in case of success or a failure notification). - - \hbugs{} tutors act as MONET services. - -\section{An \hbugs{} Session Example} -\label{usage} -In this section we describe a typical \hbugs{} session. The aim of the -session is to solve the following easy exercise: -\begin{exercise} -Let $x$ be a generic real number. Using the \helm{} proof-engine, -prove that -\begin{displaymath} -x = \frac{(x+1)*(x+1) - 1 - x*x}{2} -\end{displaymath} -\end{exercise} - -Let us suppose that the \hbugs{} broker is already running and that the -tutors already registered themselves to the broker. -When the user starts our proof-engine \texttt{gTopLevel}, the system registers itself to -the broker, that sends back the list of available tutors. By default, -\texttt{gTopLevel} notifies to the broker its intention of subscribing to every -tutor available. The user can always open a configuration window where she -is presented the list of available tutors and she can independently subscribe -and unsubscribe herself to each tutor. - -\myincludegraphics{step1}{t}{12cm}{Example session.} - {Example session.} -%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.} -% {Example session, snapshot 2.} - -The user can now insert into the system the statement of the theorem and start -proving it. Let us suppose that the first step of the user is proving -that the denominator 2 is different from 0. Once that this technical result -is proven, the user must prove the goal shown in the upper right corner -of the window in background in Fig. \ref{step1}. - -While the user is wondering how to proceed in the proof, the tutors are -trying to progress in the proof. After a while, the tutors' suggestions -start to appear in the lower part of the \hbugs{} interface window -(the topmost window in Fig. \ref{step1}). In this case, the tutors are able -to produce 23 hints. The first and not very useful hint suggests to proceed in -the proof by exchanging the two sides of the equality. -The second hint suggests to reduce both sides of the equality to their normal -form by using only reductions which are justified by the ring structure of the -real numbers; the two normal forms, though, are so different that the proof is -not really simplified. -All the residual 21 hints suggest to apply one lemma from the distributed -library of \helm{}. The user can look at the statement of any lemma by clicking -on its URI. - -The user can now look at the list of suggestions and realize that a good one is -applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality -members by the same scalar\footnote{Even if she does not receive the hint, the -user probably already knows that this is the right way to proceed. The -difficult part, accomplished by the hint, is guessing what is the name of the -lemma to apply.}. -Double-clicking on the hint automatically applies -the lemma, reducing the proof to closing three new goals. The first one asks -the user the scalar to use as an argument of the previous lemma; the second -one states that the scalar is different from 0; the third lemma (the main -one) asks to prove the equality between the two new members. -% is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for -% the still unknown scalar argument, which can have only $H$ and $x$ as -% free variables. - -The user proceeds by instantiating the scalar with the number 2. The -\texttt{Assumption} tutor now suggests to close the second goal (that -states that $2 \neq 0$) by applying the hypothesis $H$. -No useful suggestions, instead, are generated for the main goal -$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$. -To proceed in the proof the user needs to simplify the -expression using the lemma $Rinv\_r\_simpl\_m$ that states that -$\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor -suggesting simplifications, the user must find out this simplification by -himself. Once she founds it, the goal is reduced to proving that -$2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the -\texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is -just one of the 22 hints that the user receives. It is the only hint that -does not open new goals, but the user right now does not have any way to know -that.} to the user how to complete the proof in one macrostep. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Comandi da dare a gTopLevel % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% New proof: -% !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))) -% Intros x H -% Apply r_Rmult_mult -% 3: Apply H -% Simpl (per fare unfold di Rdiv) -% Rewrite <- -% (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1))) -% Rewrite -> -% (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H) -% *** Ring -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\section{Implementation's Highlights} -\label{implementation} -In this section we present some of the most relevant implementation details of -the \hbugs{} architecture. - - - \paragraph{Proof status} - In our implementation of the \hbugs{} architecture we used the proof - assistant of the \helm{} project (codename \texttt{gTopLevel}) as an \hbugs{} - client. Thus we have implemented serialization/deserialization capabilities - for its internal status. In order to be able to describe \wss{} that - exchange status in WSDL using the XML Schema type system, we have chosen an - XML format as the target format for the serialization. - -% A schematic representation of the gTopLevel internal status is depicted in -% Fig. \ref{status}. - Each proof is represented by a tuple of four elements: - \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}. - -% \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof -% status} - - \begin{description} - \item[uri]: an URI chosen by the user at the beginning of the proof - process. Once (and if) proved, that URI will globally identify the term - inside the \helm{} library (given that the user decides to save it). - \item[thesis]: the ongoing proof thesis - \item[proof]: the current incomplete proof tree. It can contain - \emph{metavariables} (holes) that stands for the parts of the proof - that are still to be completed. Each metavariable appearing in the - tree references one element of the metavariables environment - (\emph{metasenv}). - \item[metasenv]: the metavariables environment is a list of - \emph{goals} (unproved conjectures). - In order to complete the proof, the user has to instantiate every - metavariable in the proof with a proof of the corresponding goal. - Each goal is identified by an unique identifier and has a context - and a type (the goal thesis). The context is a list of named - hypotheses (declarations and definitions). Thus the context and the goal - thesis form a sequent, which is the statement of the proof that will - be used to instantiate the metavariable occurrences. - \end{description} - - Each of these information is represented in XML as described in - \cite{mowglicic}. Additionally, an \hbugs{} status carries the unique - identifier of the current goal, which is the goal the user is currently - focused on. Using this value it is possible to implement different client - side strategies: the user could ask the tutors to work on the goal - she is considering or to work on the other ``background'' goals. - - \paragraph{Hints} - A hint in the \hbugs{} architecture should carry enough information to - permit the client to progress in the current proof. In our - implementation each hint corresponds to either one of the tactics available - to the user in gTopLevel (together with its actual arguments) or a set - of alternative suggestions (a list of hints). - - For tactics that do not require any particular argument (like tactics that - apply type constructors or decision procedures) - only the tactic name is represented in the hint. For tactics that need - terms as arguments (for example the \texttt{Apply} tactic that apply a - given lemma) the hint includes a textual representation of them, using the - same representation used by the interactive proof assistant when querying - user for terms. In order to be transmitted between \wss{}, hints are - serialized in XML. - - It is also possible for a tutor to return more hints at once, - grouping them in a particular XML element. - This feature turns out to be particularly useful for the - \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that - queries a lemma database and returns to the client a list of all lemmas that - could be used to complete the proof. This particular hint is encoded as a - list of \texttt{Apply} hints, each of them having one of the results as term - argument. - - We would like to stress that the \hbugs{} architecture has no dependency - on either the hint or the status representation: the only message parts - that are fixed are those representing the administrative messages - (the envelopes in the \wss{} terminology). In particular, the broker can - manage at the same time several sessions working on different status/hints - formats. Of course, there must be an agreement between the clients - and the tutors on the format of the data exchanged. - - In our implementation the client does not trust the tutors hints: - being encoded as references to available tactics imply - that an \hbugs{} client, at the receipt of a hint, simply try to replay - the work - done by a tutor on the local copy of the proof. The application of the hint - can even fail to type check and the client copy of the proof can be left - undamaged after spotting the error. Note, however, that it is still - possible to implement a complex tutor that looks for a proof doing - backtracking and that - send back to the client a hint whose argument is a witness (a trace) of - the proof found: the client applies the hint reconstructing (and checking - the correctness of) the proof from the witness, without having to - re-discover the proof itself. - - An alternative implementation where the tutors are trusted would simply - send back to the client a new proof-status. Upon receiving the - proof-status, the client would just override its current proof status with - the suggested one. In the case of those clients which are implemented - using proof-objects (as the Coq proof-assistant, for instance), it is - still possible for the client to type-check the proof-object and reject - wrong hints. The systems that are not based on proof-objects - (as PVS, NuPRL, etc.), instead, must completely trust the new proof-status. - In this case the \hbugs{} architecture would need at least to be extended - with clients-tutors authentication. - - \paragraph{Registries} - Being central in the \hbugs{} architecture, the broker is also responsible - of housekeeping operations both for clients and tutors. These operations are - implemented using three different data structures called \emph{registries}: - clients registry, tutors registry and \musings{} registry. - - In order to use the suggestion engine a client should register itself to the - broker and subscribe to one or more tutors. The registration phase is - triggered by the client using the \texttt{Register\_client} method of the - broker to send him an unique identifier and its base URI as a \ws{}. After - the registration, the client can use the \texttt{List\_tutors} method of the - broker to get a list of available tutors. Eventually the client can - subscribe to one or more of these using the \texttt{Subscribe} method of the - broker. Clients can also unregister from brokers using - \texttt{Unregister\_client} method. - - The broker keeps track of both registered clients and clients' subscriptions - in the clients registry. - - In order to be advertised to clients during the subscription phase, tutors - should register to the broker using the \texttt{Register\_tutor} method of - the broker. This method is really similar to \texttt{Register\_client}: - tutors are required to send an unique identifier and a base URI for their - \ws{}. - Additionally tutors are required to send an human readable description of - their capabilities; this information could be used by the client user to - decide which tutors she wants to subscribe to. As the clients, tutors can - unregister from brokers using \texttt{Unregister\_broker} method. - - Each time the client status changes, it get sent sent to the - broker using its \texttt{Status} method. Using both the clients registry (to - lookup the client's subscription) and the tutors registry (to check if some tutors - have unsubscribed), the broker is able to decide to which tutors the - new status have to be forwarded. -% \ednote{CSC: qui o nei lavori futuri parlare -% della possibilit\'a di avere un vero brocker che multiplexi le richieste -% dei client localizzando i servizi, etc.} - - The forwarding operation is performed using the \texttt{Start\_musing} - method of the tutors, that is a request to start a new computation - (\emph{\musing{}}) on a given status. The return value of - \texttt{Start\_musing} is a - \musing{} identifier that is saved in the \musings{} registry along with - the identifier of the client that triggered the \musing{}. - - As soon as a tutor completes an \musing{}, it informs the broker - using its \texttt{Musing\_completed} method; the broker can now remove the - \musing{} entry from the \musings{} registry and, depending on its outcome, - inform the client. In case of success one of the \texttt{Musing\_completed} - arguments is a hint to be sent to the client; otherwise there is no need to - inform him and the \texttt{Musing\_completed} method is called - just to update the \musings{} registry. - - Consulting the \musings{} registry, the broker is able to know, at each - time, which \musings{} are in execution on which tutor. This peculiarity is - exploited by the broker on invocation of the \texttt{Status} method. - Receiving a new status from the client implies indeed that the previous - status no longer exists and all \musings{} working on it should be stopped: - additionally to the already described behavior (i.e. starting new - \musings{} on the received status), the broker takes also care of stopping - ongoing computation invoking the \texttt{Stop\_musing} method of the tutors. - -%CASSATO -% \paragraph{\wss{}} -% As already discussed, all \hbugs{} actors act as \wss{} offering one or more -% services to neighbor actors. To grant as most accessibility as possible to -% our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given -% that our proof assistant was entirely developed in the Objective Caml -% language, we have chosen to develop also \hbugs{} in that language in order -% to maximize code reuse. To develop \wss{} in Objective Caml we have -% developed an auxiliary generic library (\emph{O'HTTP}) that can be used to -% write HTTP 1.1 Web servers and abstracts over GET/POST parsing. This library -% supports different kinds of Web servers architectures, including -% multi-process and multi-threaded ones.} bindings described in -% \cite{wsdlbindings}. - - \paragraph{Tutors} - Each tutor exposes a \ws{} interface and should be able to work, not only for - many different clients referring to a common broker, but also for many - different brokers. The potential high number of concurrent clients imposes - a multi-threaded or multi-process architecture. - - Our current implementation is based on a multi threaded architecture - exploiting the capabilities of the O'HTTP library \cite{zack}. Each tutor is - composed by one always running thread plus an additional thread for each - \musing{}. - One thread is devoted to listening for incoming \ws{} requests; when a - request is received the control is passed to a second thread, created on the - fly, that handle the incoming request (usual one-thread-per-request approach - in web servers design). - In particular if the received request is \texttt{Start\_musing}, a new thread is - spawned to handle it; the thread in duty to handle the HTTP request - returns an HTTP response containing the identifier of the just started - \texttt{musing}, and then dies. If the received request is - \texttt{Stop\_musing}, instead, the spawned thread kills the thread - responsible for the \texttt{musing} whose identifier is the argument - of the \texttt{Stop\_musing} method. - - This architecture turns out to be scalable and allows the running threads - to share the cache of loaded (and type-checked) theorems. - As we will explain in Sect. \ref{tutors}, this feature turns out to be - really useful for tactics that rely on a huge but fixed set of lemmas, - as every reflexive tactic. - - The implementation of a tutor within the described architecture is not that - difficult having a language with good threading capabilities (as OCaml has) - and a pool of already implemented tactics (as \texttt{gTopLevel} has). - Working with threads is known to be really error prone due to - concurrent programming intrinsic complexity. Moreover, there is a - non-neglectable part of code that needs to be duplicated in every tutor: - the code to register the tutor to the broker and to handle HTTP requests; - the code to manage the creation and termination of threads; and the code for - parsing the requests and serializing the answers. As a consequence we - have written a generic implementation of a tutor which is parameterized - over the code that actually proposes the hint and over some administrative - data (as the port the tutor will be listening to). - - The generic tutor skeleton is really helpful in writing new tutors. - Nevertheless, the code obtained by converting existing tactics into tutors - is still quite repetitive: every tutor that wraps a tactic has to - instantiate its own copy of the proof-engine kernel and, for each request, - it has to override its status, guess the tactic arguments, apply the tactic - and, in case of success, send back a hint with the tactic name and the - chosen arguments. Of course, the complex part of the work is guessing the - right arguments. For the simple case of tactics that do not require - any argument, though, we are able to automatically generate the whole - tutor code given the tactic name. Concretely, we have written a - tactic-based tutor template and a script that parses an XML file with - the specification of the tutor and generates the tutor's code. - The XML file describes the tutor's port, the code to invoke the tactic, - the hint that is sent back upon successful application and a - human readable explanation of the tactic implemented by the tutor. - -\section{The Implemented \hbugs Tutors} -\label{tutors} -To test the \hbugs{} architecture and to assess the utility of a suggestion -engine for the end user, we have implemented several tutors. In particular, -we have investigated three classes of tutors: -\begin{enumerate} - \item \emph{Tutors for beginners}. These are tutors that implement tactics - which are neither computationally expensive nor difficult to understand: - an expert user can always understand if the tactic can be applied or not - without having to try it. For example, the following implemented tutors - belong to this class: - \begin{itemize} - \item \emph{Assumption Tutor}: it ends the proof if the thesis is - equivalent\footnote{In our implementation, the equivalence relation - imposed by the logical framework is \emph{convertibility}. Two - expressions are convertible when they reduce to the same normal form. - Two ``equal'' terms depending on free variables can be non-convertible - since free variables stop the reduction. For example, $2x$ is convertible - with $(3-1)x$ because they both reduce to the same normal form - $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is - already in normal form.} - to one of the hypotheses\footnote{ - In some cases, especially when non-trivial computations are involved, - the user is totally unable to figure out the convertibility of two terms. - In these cases the tutor becomes handy also for expert users.}. - \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad - adsurdum} if one hypothesis is equivalent to $False$. - \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it - suggests to apply the commutative property. - \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}: - the Constructor Tutor suggests to proceed in the proof by applying one - or more constructors when the goal thesis is an inductive type or a - proposition inductively defined according to the declarative - style\footnote{An example of a proposition that can be given in - declarative style is the $\le$ relation over natural numbers: - $\le$ is the smallest relation - such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such - that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof - of $n \le n$ is simply the application of the first constructor to - $n$ and a proof of $n \le m$ is the application of the second - constructor to $n,m$ and a proof of $n \le m$.}. - Since disjunction, conjunction, existential quantification and - Leibniz equality are particular cases of inductive propositions, - all the other tutors of this class are instantiations of the - the Constructor tactic. Left and Right suggest to prove a disjunction - by proving its left/right member; Split reduces the proof of a - conjunction to the two proof of its members; Exists suggests to - prove an existential quantification by providing a - witness\footnote{This task is left to the user.}; Reflexivity proves - an equality whenever the two sides are convertible. - \end{itemize} - Beginners, when first faced with a tactic-based proof-assistant, get - lost quite soon since the set of tactics is large and their names and - semantics must be remembered by heart. Tutorials are provided to guide - the user step-by-step in a few proofs, suggesting the tactics that must - be used. We believe that our beginners tutors can provide an auxiliary - learning tool: after the tutorial, the user is not suddenly left alone - with the system, but she can experiment with variations of the exercises given - in the tutorial as much as she like, still getting useful suggestions. - Thus the user is allowed to focus on learning how to do a formal proof - instead of wasting efforts trying to remember the interface to the system. - \item \emph{Tutors for Computationally Expensive Tactics}. Several tactics have - an unpredictable behavior, in the sense that it is unfeasible to understand - whether they will succeed or they will fail when applied and what will be - their result. Among them, there are several tactics either computationally - expensive or resource consuming. In the first case, the user is not - willing to try a tactic and wait for a long time just to understand its - outcome: she would prefer to keep on concentrating on the proof and - have the tactic applied in background and receive out-of-band notification - of its success. The second case is similar, but the tactic application must - be performed on a remote machine to avoid overloading the user host - with several concurrent resource consuming applications. - - Finally, several complex tactics and in particular all the tactics based - on reflexive techniques depend on a pretty large set of definitions, lemmas - and theorems. When these tactics are applied, the system needs to retrieve - and load all the lemmas. Pre-loading all the material needed by every - tactic can quickly lead to long initialization times and to large memory - footstamps. A specialized tutor running on a remote machine, instead, - can easily pre-load the required theorems. - - As an example of computationally expensive task, we have implemented - a tutor for the \emph{Ring} tactic \cite{ringboutin}. - The tutor is able to prove an equality over a ring by reducing both members - to a common normal form. The reduction, which may require some time in - complex cases, - is based on the usual commutative, associative and neutral element properties - of a ring. The tactic is implemented using a reflexive technique, which - means that the reduction trace is not stored in the proof-object itself: - the type-checker is able to perform the reduction on-the-fly thanks to - the conversion rules of the system. As a consequence, in the library there - must be stored both the algorithm used for the reduction and the proof of - correctness of the algorithm, based on the ring axioms. This big proof - and all of its lemmas must be retrieved and loaded in order to apply the - tactic. The Ring tutor loads and caches all the required theorems the - first time it is contacted. - \item \emph{Intelligent Tutors}. Expert users can already benefit from the previous - class of tutors. Nevertheless, to achieve a significative production gain, - they need more intelligent tutors implementing domain-specific theorem - provers or able to perform complex computations. These tutors are not just - plain implementations of tactics or decision procedures, but can be - more complex software agents interacting with third-parties software, - such as proof-planners, CAS or theorem-provers. - - To test the productivity impact of intelligent tutors, we have implemented - a tutor that is interfaced with the \helm{} - Search-Engine\footnote{\url{http://helm.cs.unibo.it/library.html}} and that - is able to look for every theorem in the distributed library that can - be applied to proceed in the proof. Even if the tutor deductive power - is extremely limited\footnote{We do not attempt to check if the new goals - obtained applying a lemma can be automatically proved or, even better, - automatically disproved to reject the lemma.}, it is not unusual for - the tutor to come up with precious hints that can save several minutes of - work that would be spent in proving again already proven results or - figuring out where the lemmas could have been stored in the library. -\end{enumerate} - -\section{Conclusions and Future Work} -\label{conclusions} - In this paper we described a suggestion engine architecture for - proof-assistants: the client (a proof-assistant) sends the current proof - status to several distributed \wss{} (called tutors) that try to progress - in the proof and, in case of success, send back an appropriate hint - (a proof-plan) to the user. The user, that in the meantime was able to - reason and progress in the proof, is notified with the hints and can decide - to apply or ignore them. A broker is provided to decouple the clients and - the tutors and to allow the client to locate and invoke the available remote - services. The whole architecture is an instance of the MONET architecture - for Mathematical \wss{}. It constitutes a reimplementation of the core - features of the pioneering \OmegaAnts{} system in the new \wss{} - framework. - - A running prototype has been implemented as part of the - \helm{} project \cite{helm} - and we already provide several tutors. Some of them are simple tutors that - try to apply one or more tactics of the \helm{} Proof-Engine, which is also - our client. We also have a much more complex tutor that is interfaced - with the \helm{} Search-Engine and looks for lemmas that can be directly - applied. - - Future works comprise the implementation of new features and tutors, and - the embedding of the system in larger test cases. For instance, one - interesting case study would be interfacing a CAS as Maple to the - \hbugs{} broker, developing at the same time a tutor that implements the - Field tactic of Coq, which proves the equality of two expressions in an - abstract field by reducing both members to the same normal form. CASs can - produce several compact normal forms, which are particularly informative - to the user and that may suggest how to proceed in a proof. Unfortunately, - CASs do not - provide any certificate about the correctness of the simplification. On - the contrary, the Field tactic certifies the equality of two expressions, - but produces normal forms that are hardly a simplification of the original - formula. The benefits for the CAS would be obtained by using the Field tutor - to certify the CAS simplifications, proving that the Field normal form - of an expression is preserved by the simplification. - More advanced tutors could exploit the CAS to reduce the - goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor - certify the simplification according to the skeptical approach. - - We have many plans for further developing both the \hbugs{} architecture and - our prototype. Interesting results could be obtained - augmenting the informative content of each suggestion. We can for example - modify the broker so that also negative results are sent back to the client. - Those negative suggestions could be reflected in the user interface by - deactivating commands to narrow the choice of tactics available to the user. - This approach could be interesting especially for novice users, but requires - the client to increase their level of trust in the other actors. - - We plan also to add some rating mechanism to the architecture. A first - improvement in this direction could be distinguishing between hints that, when - applied, are able to completely close one or more goals, and - tactics that progress in the proof by reducing one or more goals to new goals: - since the new goals can be false, the user can be forced later on to - backtrack. - - Other heuristics and or measures could be added to rate - hints and show them to the user in a particular order: an interesting one - could be a measure that try to minimize the size of the generated proof, - privileging therefore non-overkilling solutions \cite{ring}. - - We are also considering to follow the \OmegaAnts{} path adding - ``recursion'' to the system so that the proof status resulting from the - application of old hints are cached somewhere and could be used as a starting - point for new hint searches. The approach is interesting, but it represents - a big shift towards automatic theorem proving: thus we must consider if it is - worth the effort given the increasing availability of automation in proof - assistants tactics and the ongoing development of \wss{} based on - already existent and well developed theorem provers. - - Even if not strictly part of the \hbugs{} architecture, the graphical user - interface (GUI) of our prototype needs a lot of improvement if we want - it to be really usable by novices. In particular, a critical issue - is avoiding continuous distractions for the user determined by the hints - that are asynchronously pushed to her. - - Our \wss{} still lack a real integration in the MONET architecture, - since we do not provide the different ontologies to describe our problems, - solutions, queries, and services. In the short term, completing this task - could provide a significative feedback to the MONET consortium and would - enlarge the current set of available MONET actors on the Web. In the long - term, new more intelligent tutors could be developed on top of already - existent MONET \wss{}. - - To conclude, \hbugs{} is a nice experiment meant to understand whether the - current \wss{} technology is mature enough to have a concrete and useful - impact on the daily work of proof-assistants users. So far, only the tutor - that is interfaced with the \helm{} Search-Engine has effectively increased - the productivity of experts users. The usefulness of the tutors developed for - beginners, instead, need further assessment. - -\begin{thebibliography}{01} - -\bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\ - \url{http://www.w3.org/TR/2003/WD-ws-gloss-20030514/} - -\bibitem{wsdlbindings} Web Services Description Language (WSDL) - Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\ - \url{http://www.w3.org/TR/wsdl12-bindings/} - -\bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and - Deduction Systems via the Logic Broker Architecture. In Proceedings - of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000. - -\bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of - the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz, - Austria, May 2002. - -\bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena. - Mathematical Knowledge Management in HELM. In Annals of Mathematics and - Artificial Intelligence, 38(1): 27--46, May 2003. - -\bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach - at Combining Interactive and Automated Theorem Proving. In M. Kerber and - M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp. - 81--97, 2000. - -\bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge. - Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.), - Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier. - -\bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, - X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, - W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical - Assistant. In W. McCune (ed), Proceedings of the 14th Conference on - Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255, - Townsville, Australia, 1997. - -\bibitem{ringboutin} S. Boutin. Using reflection to build efficient and - certified decision procedures. In Martin Abadi and Takahashi Ito, editors, - TACS'97, volume 1281. LNCS, Springer-Verlag, 1997. - -\bibitem{maplemodeforCoq} David Delahaye, Micaela Mayero. - A Maple Mode for Coq. Contribution to the Coq library.\\ - \url{htpp://coq.inria.fr/contribs/MapleMode.html} - -\bibitem{MONET-Overview} The MONET Consortium, MONET Architecture Overview, - Public Deliverable D04 of the MONET Project.\\ - \url{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf} - -\bibitem{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable - D2.a.\\ - \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html} - -\bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the - Bad Habit of Overkilling. In Supplementary Proceedings of the 14th - International Conference TPHOLS 2001, pp. 352--367, Edinburgh. - -\bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla - dimostrazione interattiva}, Master Thesis, University of Bologna, 2002. - -\bibitem{ws3} J. Zimmer and M. Kohlhase. System Description: The MathWeb - Software Bus for Distributed Mathematical Reasoning. - In Proceedings of the 18th International Conference on Automated Deduction - CADE 18, LNAI 2392, Springer Verlag, 2002. - -\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible - Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999. - -\end{thebibliography} - -\end{document}