[helm.git] / helm / papers / calculemus-2003 / hbugs-calculemus-2003.tex

\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, CAS 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 this 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 try to make progress in the proof and, in case
  of success, notify 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 in 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{} are 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 present 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 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, the comparison with \Omegapp{} is less interesting since the
  functionalities we provide so far are clearly a subset of the ones of
  \OmegaAnts.

  \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. More structured hints can also be used: 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 for the broker (to receive hints)
    and as requesters (to submit new status). Clients
    additionally use broker service 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) and hints are shown to
    the user be the means of some effect 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{} client and tutors contact the
    Getter (a MONET Mathematical Object Manager) to locate and retrieve
    mathematical items in 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 a new problem. 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, however,
    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 component 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 \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 the system 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 the 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 where the hint helps 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 directly finish the proof.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%    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 ``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 thesis of the ongoing proof
      \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 carry 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 don't 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
    query a lemma database and return 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 envelops 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, upon receival 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
    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, have to trust the new proof-status. In this
    case the \hbugs{} architecture needs 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 broker's
    \texttt{List\_tutors} method to get a list of available tutors.
    Eventually the client can subscribe to one or more of these using broker's
    \texttt{Subscribe} method. 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 broker's \texttt{Register\_tutor}
    method.  This method is really similar to \texttt{Register\_client}:
    tutors are required to send an unique identify 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 client's user to
    decide which tutors he needs to subscribe to. As the clients, tutors can
    unregister from brokers using \texttt{Unregister\_broker} method.

    Each time the client status change, it get sent sent to the
    broker using its \texttt{Status} method. Using both clients registry (to
    lookup client's subscription) and tutors registry (to check if some tutors
    has 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's 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.

  \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 abstract over GET/POST parsing. This library
    supports different kinds of Web servers architecture, including
    multi-process and multi-threaded ones.} bindings described in
    \cite{wsdlbindings}.

  \paragraph{Tutors}
    Each tutor expose 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. Each tutor is composed
    by one thread always running plus
    an additional thread for each running \musing{}. One thread is devoted to
    listening for incoming \ws{} request; upon correct receiving requests it
    pass the control to a second thread, created on the fly, to handle the
    incoming request following the classical one-thread-per-request approach in
    web servers design.
    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 dyes. 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 with 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 gTopLevel has).
    Still 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 propose the hint and 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 proof 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{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 resources 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 cache all the required theorems the
  first time it is contacted.
 \item{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{}.

  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. CAS can
  produce several compact normal forms, which are particularly informative
  to the user and help in proceeding in a proof. Unfortunately, CAS 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 require
  the client to trust other actors a bit more than in the current approach.

  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:
  the new goals could be false and the proof can be closed only by backtracking.

  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 more closely 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 would like
  it to be really usable by novices. In particular, the user is too easily
  distracted by the tutor's hints that are ``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}