\end{figure}
}
-\usepackage[show]{ed}
-\usepackage{draftstamp}
+%\usepackage[show]{ed}
+%\usepackage{draftstamp}
\newcommand{\musing}{\texttt{musing}}
\newcommand{\musings}{\texttt{musings}}
\title{Brokers and Web-Services for Automatic Deduction: a Case Study}
-\author{Claudio Sacerdoti Coen \and Stefano Zacchiroli}
+\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\\
\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 an
- interactive proof-assistant. When the broker is submitted a "proof status" (an
- unfinished 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.
+ 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 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 \ednote{zack: buhm! :-P} is providing a further level of
- stable services (called \emph{brokers}) that behave as common gateway/address
- for client applications to access a wide variety of services and abstract over
- them.
+ 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}}
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 client of these
+ 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 extremely low and the concrete benefits are still to be assessed.
+ 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
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.
+ 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
+ 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.
+ 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{} are that the latter is based on a
+ between \hbugs{} and \OmegaAnts{} is that the latter is based on a
black-board architecture and it is not implemented using \wss{} and
- brokers. Other differences will be detailed in Sect. \ref{conclusions}
- \ednote{CSC: che si fa di sta frase?}.
+ 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 paper ends with the conclusions and future works.
+ As usual, the final section of this paper is devoted to conclusions and future works.
\section{An \hbugs{} Bird's Eye View}
\label{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{}
+ Each actor presents one or more \ws{} interfaces to its neighbors \hbugs{}
actors.
- In this section we will detail the role and requirements of each kind of
- actors and discuss about the correspondences between them and the MONET
+ 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
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. An hint is a
- representation\ednote{CSC: non c'\'e un sinonimo pi\'u carino? Zack: l'unico
- decente sembra essere nuovamente "suggestion". CSC: chiamalo sinonimo!}
- of a step that can be performed in order to proceed in 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: an hint can be
+ parameters. Hints can also be more structured: a hint can be
as complex as a whole proof-plan.
- \myincludegraphics{interfaces}{t}{10cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
- \wss{} interfaces}
-
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.
+ 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 role of client is taken by an interactive proof assistant,
+ 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).\ednote{CSC: questo \'e un
- possibile posto dove mettere una mini-sessione interattiva. L'appendice
- un altro.}
+ 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{} client and tutors contact 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 in the \helm{} library.
+ 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 are given an unique identifier (URI) to be managed by the
+ 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 client, a broker act as \ws{} provider, receiving the
+ 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 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{}
- \ednote{Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo
- commento sulla utilita'/quantita' delle figure ... CSC: vanno benissimo}
+ 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.
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 it is
+ 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).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i
- multi-sessione. Ma mi sembra la strada che prenderemmo, no?}
-
- The MONET architecture specification does not state explicitly whether
- the service and broker answers can be asynchronous. Nevertheless, the
+ 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
appropriate actor's method.
\paragraph{Tutors}
- Tutors are software component able to consume proof status producing hints.
- \hbugs{} doesn't specify by which means hints should be produced: tutors can
- use any means necessary (heuristics, external theorem prover or CAS, ...).
- 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. As
+ 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 (an hint in case of success or a notification of failure).
+ 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
\paragraph{Proof status}
In our implementation of the \hbugs{} architecture we used the proof
- assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
+ 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:
+% 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}
+% \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[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
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
+ 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
+ \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}
- An hint in the \hbugs{} architecture should carry enough information to
+ 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
+ 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
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
+ 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 envelops in the \wss{} terminology). In particular, the broker can
+ (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, on receipt of an hint, simply try to reply the work
+ 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
- send back to the client an hint whose argument is a witness (a trace) of
+ 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.
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.
+ (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
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
+ 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 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
+ 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 client's user to
- decide which tutors he needs to subscribe to. Like clients, tutors can
+ 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 change, the status is sent to the
- broker using its \emph{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 must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
- della possibilit\'a di avere un vero brocker che multiplexi le richieste
- del tutor localizzando i servizi, etc.}
+ 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
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 an hint to be sent to the client, otherwise there's no need to
+ 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 tutor\ednote{CSC: ma \'e vero o
- stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
- ovviamente ... CSC: ma a che serve???} 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 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 tutor\ednote{CSC: Ma sei veramente veramente sicuro?}
- takes also care of stopping ongoing computation invoking
- \texttt{Stop\_musing} tutors' method.
-
- \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 bindings
- described in \cite{wsdlbindings}\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.}.
+ 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 expose a \ws{} interface and should be able to work, not only for
+ 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. Each tutor is composed
- by two 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 the second always-running thread which handle the pool
- of running \musings{}. When a new \musing{} is requested, a new thread is
- spawned to work them out; when a request to interrupt an old \musing{} is
- received, the thread actually running them is killed freeing its
- resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
- ricordo male al problema dell'uccisione dei thread. Ora o si spiega
- il motivo di questa architettura o si glissa/bluffa. Zack: cosa ti sembra
- delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...
- CSC: la motivazione per avere due thread always running e non due}
-
+ 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 reflexivite tactic.
+ as every reflexive tactic.
- The implementation of a tutor with the described architecture is not that
+ 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 gTopLevel has).
- Still working with threads is known to be really error prone due to
+ 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 propose the hint and some administrative
+ 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.
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 an hint with the tactic name and the
+ 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
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: $\le$ is the smallest relation
+ 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
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
+ 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{Tutors for Computationally Expensive Tactics}. Several tactics have
+ \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 resources consuming. In the first case, the user is not
+ 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
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
+ tactic. The Ring tutor loads and caches all the required theorems the
first time it is contacted.
- \item{Intelligent Tutors}. Expert users can already benefit from the previous
+ \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
To test the productivity impact of intelligent tutors, we have implemented
a tutor that is interfaced with the \helm{}
- Search-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ 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
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{}.
+ 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}
with the \helm{} Search-Engine and looks for lemmas that can be directly
applied.
- We have many plan for further developing both the \hbugs{} architecture and
+ 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 require
- the client to trust other actors a bit more than in the current approach.
+ 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 to distinguish between hints that, when
- applied, are able to completely close one or more goals and
+ 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.
+ 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
+ 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 proof status resulting from the
+ 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
+ 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.
+ 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
+ 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
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 users of proof-assistants. So far, only the tutor
+ 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/ws-gloss/}
+ \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.\\
Deduction Systems via the Logic Broker Architecture. In Proceedings
of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
-\bibitem{ws3} O. Caprotti. Symbolic Evaluator Service. Project Report of
+\bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
Austria, May 2002.
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{zack} S. Zacchiroli. \emph{Web services per il supporto alla
dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
-\bibitem{ws4} J. Zimmer and L. Dennis. Inductive Theorem Proving and
- Computer Algebra in the MathWeb Software Bus. In Proceedings of the 10th
- CALCULEMUS Symposium 2002, 3--5 July 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{ws2} R. Zippel. The MathBus. In Workshop on Internet Accessible
+\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
\end{thebibliography}
projects / helm.git / blobdiff