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
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 formers are implemented on top of
- Computer Algebra Systems; the latters provide interfaces to well-known
+ 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
Sect. \ref{tutors} is an overview of the tutors that have been implemented.
As usual, the paper ends with the conclusions and future works.
-\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}
\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
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 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
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
+ 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{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}
projects / helm.git / commitdiff