\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{}.
- An usage session is shown in Sect. \ref{usage}.
+ 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.
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