\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}
\end{figure}
}
-\newcommand{\todo}[1]{\footnote{\textbf{TODO: #1}}}
+\usepackage[show]{ed}
+\usepackage{draftstamp}
+
\newcommand{\ws}{Web-Service}
\newcommand{\wss}{Web-Services}
\newcommand{\hbugs}{H-Bugs}
\newcommand{\helm}{HELM}
+\newcommand{\Omegapp}{$\Omega$mega}
+\newcommand{\OmegaAnts}{$\Omega$mega-Ants}
\title{Brokers and Web-Services for Automatic Deduction: a Case Study}
\end{abstract}
\section{Introduction}
- The \ws\ approach at software development seems to be a working solution for
+ 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\
+ grant longevity and implementations availability for frameworks based on \wss{}\
for information exchange. As a direct conseguence, the number of such
- frameworks in increasing and the World Wide Web is moving from a disorganized
+ 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
and output.
- 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 \todo{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.
-
- Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET} 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. This
- framework turns out to be strongly based on both \wss\ and brokers.
-
- 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
- \todo{citarne qualcuno: CSC???}. On the other hand \todo{troppo informale?}
- the set of \wss\ related to Proof Assistants tends to be ... rather ...
- empty!\todo{gia' mi immagino il tuo commento: BUHM! :-)}
+ 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 \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
+ \helm{} project. 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
+ 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
+ between \hbugs{} and \OmegaAnts{} is that the latter is based on a
+ black-board architecture and it is not implemented using \wss{} and
+ brokers. Other differences will be detailed in Sect. \ref{conclusions}.
+ 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
+ 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\
+ 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
+ \ws{} interfacing a CAS to simplify expressions in a particular mathematical
domain.
+}
- The Omega Ants project \todo{date, autori e paperi}, developed before the
- \emph{\ws\ era}, enrich the Omega \cite{Omega} proof assistant with an
- architecture able to distribute subparts of a proof to agents (Ants)
- implemented as separate processes running on the same hosts of the proof
- assistant \todo{controllare ...}.
+\section{Architecture}
+\label{architecture}
+ \myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
- 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. This architecture is based on a set of \wss\ and a broker (a
- \ws\ itself) and is able to distribute a proof status from a client to several
- \emph{tutor}, each of them can try to make progress in the proof and, in case
- of success, notify the user sending him an \emph{hint}. Both the broker and
- the tutors are instances of the homonymous entities of the MONET framework.
+ 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