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
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 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
+ The standard solution 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.
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.
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{omegaants},
- which provided similar functionalities to the
+ 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}
- \ednote{CSC: che si fa di sta frase?}.
+ brokers.
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}
+\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}
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. An 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
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}
+ 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 (chosing the available tutors among the ones to
+ 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?}
+ URL).
- The MONET architecture specification does not state explicitely whether
- the service and broker answers can be asyncronous. Nevertheless, the
- described information flow implicitly suggests a syncronous implementation.
- On the contrary, in \hbugs{} every request is asyncronous: the connection
+ 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.
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
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
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 trasmitted between \wss{}, hints are
+ 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
+ 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
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 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:
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
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 autentication.
+ clients-tutors authentication.
\paragraph{Registries}
Being central in the \hbugs{} architecture, the broker is also responsible
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.}
+ 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
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
+ 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 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 behaviour (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.
+ the already described behavior (i.e. starting new \musings{} on the
+ received status), the broker 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{wsdlbindings}\footnote{Given that our proof assistant was
entirely developed in the Objective Caml language, we have chosen to
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 successfull application and a
+ 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
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
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
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.
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 expecially for novice users, but require
+ 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 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 backtraking.
+ 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
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 usefullness of the tutors developed for
+ the productivity of experts users. The usefulness of the tutors developed for
beginners, instead, need further assessment.
\begin{thebibliography}{01}
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{omegaants} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
+\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{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}
\end{document}
projects / helm.git / blobdiff