\institute{
Department of Computer Science\\
University of Bologna\\
- Via di Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
+ Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
\email{sacerdot@cs.unibo.it}
\and
Department of Computer Science\\
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 successfull results, and send them back to the
+ 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
and beginners (who can learn from it).
\end{abstract}
-\section{Introduction\ednote{Zack: attualmente sembra che posto ne abbiamo: se
-la situazione non muta un 10 righe su \helm{} possiamo metterle, non tanto per
-la conferenza quanto per i posteri}}
+\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 conseguence, the number of such
+ \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
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.
-
- \oldpart Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
- following the guidelines \ednote{guidelines non e' molto appropriato, dato che
- il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers
- approach, is working on the development of a framework aimed at providing a
- set of software tools for the advertisement and discovering of mathematical
- \wss{}.
- \begin{newpart}Since the \emph{Declaration of Linz}, the MONET Consortium
- \cite{MONET}, is working on the development of a framework, based on the
- \wss{}/brokers approac, aimed at providing a set of software tools for the
- advertisement and the discovery of mathematical \wss{}.\end{newpart}
+ 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 \wss{} providing both computational and
- reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
- dalle conferenze calculemus}: the formers are implemented on top of
- Computer Algebra Systems; the latters provide interfaces to well-known
- theorem provers. Proof-planners, proof-assistants, CAS and
+ 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 client 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.
In this paper we present an architecture, namely \hbugs{}, implementing a
\emph{suggestion engine} for the proof assistant developed on behalf of the
- \helm{} project. We provide several \wss{} (called \emph{tutors}) able to
+ \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 distribute a proof
+ 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.
- Both the broker and the tutors are instances of the homonymous entities of
- the MONET framework.
-
- A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
- which provided similar functionalities to the
- \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
+ 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. Other differences will be detailed in Sect. \ref{conclusions}.
+ brokers. Other differences will be detailed in Sect. \ref{conclusions}
+ \ednote{CSC: che si fa di sta frase?}.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
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.
-\oldpart
-{CSC: Non so se/dove mettere queste parti.
- Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
- non e' molto utile, ma la seconda sugli usi tipici di proof assistant
- come ws client si}
-{
- Despite of that the proof assistant case seems to be well suited to
- investigate the usage of many different mathematical \wss{}. Indeed: most
- proof assistants are still based on non-client/server architectures, are
- application-centric instead of document-centric, offer a scarce level of
- automation leaving entirely to the user the choice of which macro (usually
- called \emph{tactic}) to use in order to make progress in a proof.
-
- The average proof assistant can be, for example, a client of a \ws{}\
- interfacing a specific or generic purpose theorem prover, or a client of a
- \ws{} interfacing a CAS to simplify expressions in a particular mathematical
- domain.
-}
-
-\section{An \hbugs{} Bird'S Eye View\ednote{Zack: sono in vena di boiate
-stasera!}}
+\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 neighbours \hbugs{}
+ Each actor present 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 correspondencies between them and the MONET
+ actors and discuss about the correspondences between them and the MONET
entities described in \cite{MONET-Overview}.
\paragraph{Clients}
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"}
+ decente sembra essere nuovamente "suggestion". CSC: chiamalo sinonimo!}
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
as complex as a whole proof-plan.
- \myincludegraphics{interfaces}{t}{8cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
+ \myincludegraphics{interfaces}{t}{10cm}{\hbugs{} \wss{} interfaces}{\hbugs{}
\wss{} interfaces}
Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
- provider and requester, see \ednote{Zack: va bene "see"?, "cfr" credo sia
- solo italiano ...} Fig. \ref{interfaces}.
+ providers and requesters, see Fig. \ref{interfaces}.
They act as providers for the broker (to receive hints)
- and as requesters (to submit new status) \ednote{Zack: non manca il "for"
- anche per i requesters?}. Clients
+ 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.
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).
+ dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
+ possibile posto dove mettere una mini-sessione interattiva. L'appendice
+ un altro.}
\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) and Mathematical Object Manager (since proof
- status are built on the fly and not stored).
+ 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 are given an unique identifier (URI) to be managed by the
+ Getter.
\paragraph{Brokers}
Brokers are the key actors of the \hbugs{} architecture since they
With respect to client, a broker act as \ws{} provider, receiving the
proof status and forwarding it to one or more tutors.
It also acts as a \ws{} requester sending
- hints to client as soon as they are available from the tutors.
+ 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 one is accomplished
- by requesting computations (\emph{musings} in \hbugs{} terminology) on
+ 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{CSC: Sta frase va comunque riscritta perch\'e non si capisce una
- mazza. Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo commento
- sulla utilita'/quantita' delle figure ...}
+ \ednote{Zack: io intanto ho aggiunto una figura, vorrei pero' un tuo
+ commento sulla utilita'/quantita' delle figure ... CSC: vanno benissimo}
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 (chosing the available tutors among the ones to
- which the client is subscribed), Execution Manager. \ednote{non e' chiaro se
- in monet le risposte siano sincrone o meno, se cosi' fosse dobbiamo
- specificare che nel nostro caso non lo sono}
+ 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 it 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
+ 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{} 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 exists an agreement on the formats of proof
- status and hints.
+ 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
providers, they wait for commands requesting to start a new \musing{} on
\section{Implementation's Highlights}
\label{implementation}
-\ednote{Zack: l'aspetto grafico di questa parte e' un po' peso, possiamo
-aggiungere varie immagini volendo, e.g.: schema dei thread di un tutor, sample
-code di un tutor generato automaticamente}
In this section we present some of the most relevant implementation details of
the \hbugs{} architecture.
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
- fot its internal status. In order to be able to describe \wss{} that
+ 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 representated by a tuple of four elements:
+ 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
\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 metavariables appearing in the
+ 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
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 instatiate the metavariable occurrences.
+ be used to instantiate the metavariable occurrences.
\end{description}
Each of these information is represented in XML as described in
- \cite{csc-thesis}. Additionally, an \hbugs{} status carry the unique
+ \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
of alternative suggestions (a list of hints).
For tactics that don't require any particular argument (like tactics that
- apply type constructors or try to automatically conclude equality goals)
- only the tactic name is represented in the hint. For tactics that need terms
- as arguments (for example the \emph{Apply} tactic) 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
- trasmitted between \wss, hints are serialized in XML.
-
- Actually it is also possible for a tutor to return more hints at once,
+ 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 particulary useful for the
- \emph{searchPatternApply} tutor (Sect. \ref{tutors}) that
- query a term database and return to the client a list of all terms that
+ 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 Apply hints, each of them having one of the results as term
+ 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 envelops in the \wss{} terminology). In particular, the broker can
manage at the same time several sessions working on different status/hints
- formats. Of couse, there must be an agreement between the clients
+ 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:
+ 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
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 possible proof and
+ 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
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. Upong receiving the
+ 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 to be extended with clients-tutors
- autentication.
+ 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 accounting operations both for clients and tutors. These operations are
+ 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.
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\ednote{CSC: Vuoi veramente dire eventually qui? Zack: si, prima o
- poi lo faranno ...} the
- client can subscribe to one or more of these using broker's \emph{Subscribe}
- method. Clients can also unregister from brokers using
+ 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 broker's \texttt{Register\_tutor}
- method. This method is really similar to the \texttt{Register\_client}
- one: tutors are required to send an unique identify and a base URI for
- their \ws{}.
+ 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. Like clients, tutors can
unregister from brokers using \texttt{Unregister\_broker} method.
- Track of available tutors is kept in the tutors
- registry.\ednote{Non si mette mai un paragrafo lungo meno di una linea!}
-
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
della possibilit\'a di avere un vero brocker che multiplexi le richieste
del tutor localizzando i servizi, etc.}
- The forwarding operation is performed using tutors' \texttt{Start\_musing}
- method, that is a request to start a new computation (\emph{\musing{}}) on a
- given status. The return value for \texttt{Start\_musing} method is a
+ 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 starting of the \musing{}.
+ the identifier of the client that triggered the \musing{}.
- As soon as a \musing{} is completed, the owning tutor informs the broker
+ 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}
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 ...} is able to know, at each time,
+ 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 imply indeed that the previous status no longer
+ 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 behaviour (i.e. starting new \musings{} on the
- received status), the tutor takes also care of stopping ongoing computation
- invoking \texttt{Stop\_musing} tutors' method.
+ 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 neighbour actors. To grant as most accessibility as possible to
+ 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{????}\footnote{Given that our proof assistant was
+ 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
+ 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.}.
\paragraph{Tutors}
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 ...}
+ delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...
+ CSC: la motivazione per avere due thread always running e non due}
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.
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 holds the tutor's port, the code to invoke the tactic,
- the hint that is sent back upon successfull application and a
+ 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}
\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
- withouth having to try it. For example, the following implemented tutors
+ 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
$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, expecially when non-trivial computations are involved,
+ 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
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 restrictions of the
- the Constructor tactic: Left and Right suggest to prove a disjunction
+ 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
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 suddendly left alone
+ 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 behaviour, in the sense that it is unfeasible to understand
- wether they will succeed or they will fail when applied and what will be
+ 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
can easily pre-load the required theorems.
As an example of computationally expensive task, we have implemented
- a tutor for the \emph{Ring} tactic. 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,
+ 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:
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 conctacted.
+ 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
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
- Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ a tutor that is interfaced with the \helm{}
+ Search-Engine\footnote{\url{http://mowgli.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 authomatically proved or, even better,
- auhomatically disproved to reject the lemma.}, it is not unusual for
+ 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\ednote{Zack: ho scritto la parte "future
-work"}}
+\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.
+
We have many plan for further developing both the \hbugs{} architecture and
- our prototype implementing them. Interesting results could be obtained
+ 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 command narrowing the choice of tactics available to the user.
- This approach could be interesting expecially for novice users, but require
+ 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 to distinguish between hints that, when
- applied, are able to close one or more\ednote{Zack: e' possibile?} goals and
- tactics that doesn't. Other heuristics and/or measures could be added to rate
+ 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\ednote{Zack: qua se vuoi ti
- puoi pure auto-citare, cosa vuoi di piu'?}
+ 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
application of old hints are cached somewhere and could be used as a starting
- point for new hint searches. Tough the approach is interesting, it moves the
- focus closer to automatic theorem proving and we are considering if its worth
- the effort given the increasing availability of automation in proof
- assistants' tactics.
+ 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 usable by novices.\ednote{Zack: la parte della GUI non ci sta molto
- bene, sembra che vogliamo fare soldi vendendo HBugs ... forse va solo
- formulata meglio ...}
-
- Finally we hardly believe that \wss{} such our brokers and tutors could be
- used also as components uncoupled from our client, exploiting their
- capabilities is for example possible to develop a web-based proof assistant
- demonstrative application. In order to widen even more their accessibility we
- plan to write MONET descriptions \ednote{Zack: controllare se esiste un
- termine piu' preciso} of the \wss{} offered by \hbugs{} actors. For the same
- reasons we plan also to add support for Mathematical Object Managers both for
- store and retrieve proof status.
+ 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 users of proof-assistants. 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{ALF} The ALF family of proof-assistants:\\
-% {\tt http://www.cs.chalmers.se/ComputingScience/Research/\\Logic/implementation.mhtml}
-%
-% \bibitem{Coq} The Coq proof-assistant:\\
-% {\tt http://coq.inria.fr/}
-%
-% \bibitem{FORMAVIE} The Formavie project:\\
-% {\tt http://http://www-sop.inria.fr/oasis/Formavie/}
-%
-% \bibitem{EHELM} The HELM project:\\
-% {\tt http://www.cs.unibo.it/helm/}
-%
-% \bibitem{MATHWEB} The MathWeb project:\\
-% {\tt http://www.mathweb.org/}
-%
-% \bibitem{PCOQ} The PCoq project:\\
-% {\tt http://www-sop.inria.fr/lemme/pcoq/}
-%
-% \bibitem{HELM} A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
-% Towards a library of formal mathematics. Panel session of
-% the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLS'2000),
-% Portland, Oregon, USA.
-%
-% \bibitem{Ring} 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{YANNTHESIS} Y.Coscoy. \emph{Explication textuelle de preuves pour le
-% Calcul des Constructions Inductives}, PhD. Thesis, Universit\'e de Nice-Sophia
-% Antipolis, 2000.
-%
-% \bibitem{ALFA} T. Hallgreen, Aarne Ranta. An Extensible Proof Text Editor.
-% Presented at LPAR2000.
-%
-% \bibitem{Necula} G. Necula, P. Lee. Safe Kernel Extensions Without Run-Time
-% Checking. Presented at OSDI'96, October 1996.
-%
-% \bibitem{Necula2} G. Necula, P. Lee. Efficient Representation and Validation of Proofs. Presented at LICS'98, June 1998
-%
-% \bibitem{Werner} B. Werner. \emph{Une Th\'eorie des Constructions Inductives},
-% PhD. Thesis, Universit\'e Paris VII, May 1994.
+\bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
+ \url{http://www.w3.org/TR/ws-gloss/}
+
+\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{ws3} 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{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{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{ws2} 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