\title{Brokers and Web-Services for Automatic Deduction: a Case Study}
-\author{Claudio Sacerdoti Coen \and Stefano Zacchiroli}
+\author{
+ Claudio Sacerdoti Coen\thanks{Partially supported by `MoWGLI: Math on the Web, Get it by Logic and Interfaces', EU IST-2001-33562} \and
+ Stefano Zacchiroli\thanks{Partially supported by `MyThS: Models and Types for Security in Mobile Distributed Systems', EU FET-GC IST-2001-32617}}
\institute{
Department of Computer Science\\
Proof-planners, proof-assistants, CAS and
domain-specific problem solvers are natural candidates to be clients 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.
+ been insufficient to fully assess the concrete benefits of this framework.
In this paper we present an architecture, namely \hbugs{}, implementing a
\emph{suggestion engine} for the proof assistant developed on behalf of the
brokers.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
+ A usage session is shown in Sect. \ref{usage}.
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 final section of this paper is devoted to conclusions and future works.
In this section we detail the role and requirements of each kind of
actors and discuss about the correspondences between them and the MONET
entities described in \cite{MONET-Overview}.
+ Due to lack of space, we cannot compare our framework to similar proposals,
+ as the older and more advanced \Omegapp{} system. The study of the
+ correspondences with MONET is well motivated by the fact that the
+ MONET framework is still under development and that our implementation is
+ one of the first experiments in \ws-based distributed reasoning. On the
+ other hand, the comparison with \Omegapp{} is less interesting since the
+ functionalities we provide so far are clearly a subset of the ones of
+ \OmegaAnts.
\paragraph{Clients}
An \hbugs{} client is a software component able to produce \emph{proof
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 an
+ agreement on its format between clients and tutors. A 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
+ parameters. More structured hints can also be used: a hint can be
as complex as a whole proof-plan.
Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
for the client (its URL) and an unique identifier for the broker (its
URL).
+ Notice that \hbugs{} brokers have no knowledge of the domain area of
+ proof-assistants, nor they are able to interpret the messages that they
+ are forwarding. They are indeed only in charge of maintaining the
+ abstraction of several reasoning blackboards --- one for each client ---
+ of capacity one: a blackboard is created when the client submits a problem;
+ it is then ``shared'' by the client and all the tutors until the client
+ submits a new problem. Replacing the client with a CAS and all the tutors
+ with agents implementing different resolution methods for differential
+ equations would not require any change in the broker. Notice, however,
+ that all the tutors must expose the same interface to the broker.
+
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.
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 failure notification).
+ outcome (a hint in case of success or a failure notification).
\hbugs{} tutors act as MONET services.
\section{An \hbugs{} Session Example}
+\label{usage}
In this section we describe a typical \hbugs{} session. The aim of the
session is to solve the following easy exercise:
\begin{exercise}
-Let $x$ be a generic real numbers. Using the \helm{} proof-engine,
+Let $x$ be a generic real number. Using the \helm{} proof-engine,
prove that
\begin{displaymath}
x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
\end{displaymath}
\end{exercise}
-\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
- {Example session, snapshot 1.}
-%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
-% {Example session, snapshot 2.}
-
-Let us suppose that the \hbugs{} broker is already running and that several
+Let us suppose that the \hbugs{} broker is already running and that the
tutors already registered themselves to the broker.
When the user starts \texttt{gTopLevel}, the system registers itself to
the broker, that sends back the list of available tutors. By default,
-\texttt{gTopLevel} notifies the broker its intention of subscribing to every
+\texttt{gTopLevel} notifies to the broker its intention of subscribing to every
tutor available. The user can always open a configuration window where she
is presented the list of available tutors and she can independently subscribe
-and unsubscribe each tutor.
+and unsubscribe the system to each tutor.
+
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+ {Example session.}
+%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
+% {Example session, snapshot 2.}
The user can now insert into the system the statement of the theorem and start
proving it. Let us suppose that the first step of the user is proving
that the denominator 2 is different from 0. Once that this technical result
-is proven, the user must prove the goal shown in the upper left corner
+is proven, the user must prove the goal shown in the upper right corner
of the window in background in Fig. \ref{step1}.
While the user is wondering how to proceed in the proof, the tutors are
the proof by exchanging the two sides of the equality.
The second hint suggests to reduce both sides of the equality to their normal
form by using only reductions which are justified by the ring structure of the
-real numbers. The two normal forms, though, are so different that the proof is
+real numbers; the two normal forms, though, are so different that the proof is
not really simplified.
All the residual 21 hints suggest to apply one lemma from the distributed
-library of \helm{}.
+library of \helm{}. The user can look at the statement of the lemma by clicking
+on its URI.
-The user can look at the list of suggestions and realize that a good one is
-that of applying the lemma \texttt{r\_Rmult\_mult} which
-allow\footnote{The user can always look at
-the statement of a theorem by clicking on its URI.} to multiply both equality
+The user can now look at the list of suggestions and realize that a good one is
+applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
members by the same scalar\footnote{Even if she does not receive the hint, the
user probably already knows that this is the right way to proceed. The
difficult part where the hint helps is guessing what is the name of the lemma
the lemma, reducing the proof to closing three new goals. The first one asks
the user the scalar to use as an argument of the previous lemma; the second
one states that the scalar is different from 0; the third lemma (the main
-one) asks to prove the equality between the products of the two old members
-with the scalar.
+one) asks to prove the equality between the two new members.
% is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
-% the still unkown scalar argument, which can have only $H$ and $x$ as
+% the still unknown scalar argument, which can have only $H$ and $x$ as
% free variables.
-The user proceeds by istantiating the scalar with the number 2. The
-\texttt{Assumption} tutor now suggests to close the second goal by applying
-the hypothesis $H$. No useful suggestions, instead, are generated for the
-main goal $2x = 2*\frac{((x+1)*(x+1)-1-x*x)}{2}$.
-To proceed in the proof, indeed, the user needs to symplify the
+The user proceeds by instantiating the scalar with the number 2. The
+\texttt{Assumption} tutor now suggests to close the second goal (that
+states that $2 \neq 0$) by applying the hypothesis $H$.
+No useful suggestions, instead, are generated for the main goal
+$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
+To proceed in the proof the user needs to simplify the
expression using the lemma $Rinv\_r\_simpl\_m$ that states that
$\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
-suggesting symplifications, the user must find out this symplication by
+suggesting simplifications, the user must find out this simplification by
himself. Once she founds it, the goal is reduced to proving that
-$2x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
+$2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
\texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is
just one of the 22 hints that the user receives. It is the only hint that
-does not open new goals.} to the user how to directly finish the proof.
+does not open new goals, but the user right now does not have any way to know
+that.} to the user how to directly finish the proof.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Comandi da dare a gTopLevel %
she is considering or to work on the other ``background'' goals.
\paragraph{Hints}
- An hint in the \hbugs{} architecture should carry enough information to
+ A hint in the \hbugs{} architecture should carry enough information to
permit the client to progress in the current proof. In our
implementation each hint corresponds to either one of the tactics available
to the user in gTopLevel (together with its actual arguments) or a set
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
+ that an \hbugs{} client, upon receival of a hint, simply try to replay
+ 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 proof doing
backtracking and
- send back to the client an hint whose argument is a witness (a trace) of
+ send back to the client a 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.
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}
- arguments is an hint to be sent to the client, otherwise there's no need to
+ arguments is a hint to be sent to the client, otherwise there's no need to
inform him and the \texttt{Musing\_completed} method is called
just to update the \musings{} registry.
is still quite repetitive: every tutor that wraps a tactic has to
instantiate its own copy of the proof-engine kernel and, for each request,
it has to override its status, guess the tactic arguments, apply the tactic
- and, in case of success, send back an hint with the tactic name and the
+ and, in case of success, send back a hint with the tactic name and the
chosen arguments. Of course, the complex part of the work is guessing the
right arguments. For the simple case of tactics that do not require
any argument, though, we are able to automatically generate the whole
with the \helm{} Search-Engine and looks for lemmas that can be directly
applied.
+ Future works comprise the implementation of new features and tutors, and
+ the embedding of the system in larger test cases. For instance, one
+ interesting case study would be interfacing a CAS as Maple to the
+ \hbugs{} broker, developing at the same time a tutor that implements the
+ Field tactic of Coq, which proves the equality of two expressions in an
+ abstract field by reducing both members to the same normal form. CAS can
+ produce several compact normal forms, which are particularly informative
+ to the user and help in proceeding in a proof. Unfortunately, CAS do not
+ provide any certificate about the correctness of the simplification. On
+ the contrary, the Field tactic certifies the equality of two expressions,
+ but produces normal forms that are hardly a simplification of the original
+ formula. The benefits for the CAS would be obtained by using the Field tutor
+ to certify the CAS simplifications, proving that the Field normal form
+ of an expression is preserved by the simplification.
+ More advanced tutors could exploit the CAS to reduce the
+ goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
+ certify the simplification according to the skeptical approach.
+
We have many plans for further developing both the \hbugs{} architecture and
our prototype. Interesting results could be obtained
augmenting the informative content of each suggestion. We can for example
\begin{thebibliography}{01}
\bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
- \url{http://www.w3.org/TR/ws-gloss/}
+ \url{http://www.w3.org/TR/2003/WD-ws-gloss-20030514/}
\bibitem{wsdlbindings} Web Services Description Language (WSDL)
Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
+\bibitem{maplemodeforCoq} David Delahaye, Micaela Mayero.
+ A Maple Mode for Coq. Contribution to the Coq library.\\
+ \url{htpp://coq.inria.fr/contribs/MapleMode.html}
+
\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{zack} S. Zacchiroli. \emph{Web services per il supporto alla
dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
-\bibitem{ws3} 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{ws3} J. Zimmer and M. Kohlhase. System Description: The MathWeb
+ Software Bus for Distributed Mathematical Reasoning.
+ In Proceedings of the 18th International Conference on Automated Deduction
+ CADE 18, LNAI 2392, Springer Verlag, 2002.
\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
projects / helm.git / blobdiff