\newcommand{\myincludegraphics}[5]{
\begin{figure}[#2]
\begin{center}
- \includegraphics[width=#3]{XFIG-EPS/#1.eps}
+ \includegraphics[width=#3]{eps/#1.eps}
\caption[#4]{#5}
\label{#1}
\end{center}
of applications working on machine-understandable XML documents both for input
and output.
-\oldpart
-{Di effetto la prima fase. La seconda era troppo fuori-tema e dettagliata per
- un abstract}
-{
- This lack of organization along with the huge amount of documents available,
- have posed not a few problems for data location. If this limitation could be
- overcome using heuristic-based search engine for HTML pages, a satisfying
- solution has yet to be found for \ws{} location \ednote{location non mi piace, ma
- "localization" e' anche peggio, "retrieval"?}. A promising architecture seems
- to be the use of \emph{brokers}, which access point (usually an URI) is known
- by the potential clients or by \emph{registries}, to which the \wss{} subscribe
- to publish their functionalities.
-}
-\begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale
-dovrebbe essere una versione pi\'u fluida e leggera. Boh.}
-The big challenge for the next future is to provide stable and reliable
-services over this disorganized, unreliable and ever-evolving architecture.
-The standard solution is 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.
+ 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.
-Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
-following the guidelines of the \wss{}/brokers approach, is
-\end{newpart}
- working on the development of a framework aimed at providing a set of software
- tools for the advertisement and discovering of mathematical web services.
-%CSC This framework turns out to be strongly based on both \wss{} and brokers.
-\oldpart
-{Hhhmm. Chiaro il punto, ma CAS and Theorem Prover related web-services non
- \'e molto preciso.}
-{
- Several examples of CAS (Computer Algebra System) and Theorem Prover related
- \wss{} have been shown to be useful and to fit well in the MONET Architecture
- \ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?}
- the set of \wss{} related to Proof Assistants tends to be ... rather ...
- empty!\ednote{gia' mi immagino il tuo commento: BUHM! :-)}
-}
-\begin{newpart}{riformulo}
- 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
- 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.\ednote{A questo punto bisogna venire al
- sodo prima che il lettore passi al caff\'e}
-\end{newpart}
+ 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
+ web services.
+ %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 first ones are implemented on top of
+ Computer Algebra Systems; the last ones provide interfaces to well-known
+ theorem provers. Proof-planners, proof-assistants, CAS themselves 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
As usual, the paper ends with the conclusions and future works.
\oldpart
-{Non so se/dove mettere queste parti}
+{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
domain.
}
+\section{Architecture}
+\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{} interface to its neighbours \hbugs{}
+ actors.
+
+ In this section we will detail the role and requiremente of each kind of
+ actors and discuss about the correspondencies between them and the MONET
+ entities described in \cite{MONET-Overview}.
+
+ \paragraph{Clients}
+ An \hbugs{} client is a software component able to produce \emph{proof
+ status} and to consume \emph{hints}.
+
+ \ednote{"status" ha il plurale?}
+ 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 requirement exists on the proof status, but there should be an
+ agreement on its format between clients and tutors. An hint is a
+ representation of a step that can be performed in order to proceed in an
+ incomplete proof. Usually it represents a tactic available on some proof
+ assistant along with instantiation of its parameters for tactics which
+ require them.
+
+ Clients act both as \ws{} provider and requester (using W3C's terminology
+ \cite{ws-glossary}). They act as providers for the broker (to receive hints)
+ ans as requesters again for the broker (to submit new status). Clients
+ additionally use broker service to know which tutors are available and to
+ subscribe to one or more of them.
+
+ Usually, when the role of client is taken by an interactive proof assistant,
+ new status are sent to the broker as soon as the proof change (e.g. when the
+ user applies a tactic or when a new proof is started) and hints are shown to
+ the user be the means of some effect in the user interface (e.g. popping a
+ dialog box or enlightening a tactic button).
+
+ \hbugs{} clients act as MONET clients and ask broker 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).
+
+ \paragraph{Brokers}
+ \hbugs{} brokers are the key actors of the \hbugs{} architecture since they
+ act as intermediaries between clients and tutors. They act both as \ws{}
+ provider and requester \emph{both} for clients and tutors.
+
+ With respect to client, a broker act as \ws{} provider receiving status and
+ forwarding them to one or more tutors. They act as \ws{} requester sending
+ hints to client as soon as they are available from tutors.
+
+ With respect to tutors, the \ws{} provider role is accomplished by receiving
+ hints as soon as they are produced; the \ws{} requester one is accomplished
+ by requesting computations (\emph{musings} in \hbugs{} terminology) on status
+ received by clients and stopping out of date ongoing musings.
+
+ Additionally brokers keep track of available tutors and subscription of each
+ client.
+
+ \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}
+
+ \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.
+
+ tutors act both as \ws{} providers and requesters for broker. 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).
+
+ \hbugs{} tutors act as MONET services.
+
+\section{???}
+\label{implementation}
+
+\section{The \hbugs Tutors}
+\label{tutors}
+To test the \hbugs architecture and to assess the utility of a suggestion
+engine for the end user, we have implemented several tutors. In particular,
+we have investigated three classes of tutors:
+\begin{enumerate}
+ \item \emph{Tutors for beginners}. These are tutors that implement tactics
+ which are neither computationally expensive nor difficult to understand:
+ an expert user can always understand if the tactic can be applied or not
+ withouth having to try it. For example, the following implemented tutors
+ belong to this class:
+ \begin{itemize}
+ \item \emph{Assumption Tutor}: it ends the proof if the thesis is
+ equivalent\footnote{The equivalence relation is convertibility. In some
+ cases, expecially 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.}
+ to one of the hypotheses.
+ \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
+ adsurdum} if one hypothesis is equivalent to $False$.
+ \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
+ suggests to apply the commutative property.
+ \item \emph{Left/Right/Exists/Split/Constructor Tutors}: the Constructor
+ Tutor suggests to proceed in the proof by applying one or more
+ constructors when the goal thesis is an inductive type or a
+ proposition inductively defined according to the declarative style.
+ Since disjunction, conjunction and existential quantifications are
+ particular cases of inductive propositions,
+ all the other tutors of this class implements restrictions of the
+ the Constructor tactic: Left and Right suggest to prove a disjunction
+ by proving its left/right member; Split reduces the proof of a
+ conjunction to the two proof of its members; Exists suggests to
+ prove an existential quantification by providing a
+ witness\footnote{This task is left to the user.}.
+ \end{itemize}
+ Beginners, when first faced with a tactic-based proof-assistant, get
+ lost quite soon since the set of tactics is large and their names and
+ semantics must be remembered by heart. Tutorials are provided to guide
+ the user step-by-step in a few proofs, suggesting the tactics that must
+ be used. We believe that our beginners tutors can provide an auxiliary
+ learning tool: after the tutorial, the user is not suddendly 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 failt when applied and what will be
+ their result. Among them, there are several tactics either computationally
+ expensive or resources consuming. In the first case, the user is not
+ willing to try a tactic and wait for a long time just to understand its
+ outcome: she would prefer to keep on concentrating on the proof and
+ have the tactic applied in background and receive out-of-band notification
+ of its success. The second case is similar, but the tactic application must
+ be performed on a remote machine to avoid overloading the user host
+ with several concurrent resource consuming applications.
+
+ Finally, several complex tactics and in particular all the tactics based
+ on reflexive techniques depend on a pretty large set of definitions, lemmas
+ and theorems. When these tactics are applied, the system needs to retrieve
+ and load all the lemmas. Pre-loading all the material needed by every
+ tactic can quickly lead to long initialization times and to large memory
+ footstamps. A specialized tutor running on a remote machine, instead,
+ can easily pre-load the required theorems.
+
+ As an example of computationally expensive task, we have implemented
+ a tutor for the \emph{Ring} tactic. The tutor is able to prove an equality
+ over a ring by reducing both members to a common normal form. The reduction,
+ which may require some time in complex cases,
+ is based on the usual commutative, associative and neutral element properties
+ of a ring. The tactic is implemented using a reflexive technique, which
+ means that the reduction trace is not stored in the proof-object itself:
+ the type-checker is able to perform the reduction on-the-fly thanks to
+ the conversion rules of the system. As a consequence, in the library there
+ must be stored both the algorithm used for the reduction and the proof of
+ correctness of the algorithm, based on the ring axioms. This big proof
+ and all of its lemmas must be retrieved and loaded in order to apply the
+ tactic. The Ring tutor loads and cache all the required theorems the
+ first time it is conctacted.
+ \item{Intelligent Tutors}. Expert users can already benefit from the previous
+ class of tutors. Nevertheless, to achieve a significative production gain,
+ they need more intelligent tutors implementing domain-specific theorem
+ provers or able to perform complex computations. These tutors are not just
+ plain implementations of tactics or decision procedures, but can be
+ more complex software agents interacting with third-parties software,
+ such as proof-planners, CAS or theorem-provers.
+
+ To test the productivity impact of intelligent tutors, we have implemented
+ a tutor that is interfaced with the HELM
+ Proof-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
+ the tutor to come up with precious hints that can save several minutes of
+ works 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}
+
+Once the code that implements a tactic or decision procedure is available,
+transforming it into a tutor is not a difficult task, but it is surely
+repetitive and error prone.
+
+\section{???}
+\label{conclusions}
% \section{Introduction}
% Since the development of the first proof-assistants based on the
projects / helm.git / blobdiff