\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.
+RILEGGERE E CORREGGERE:
+
// certainly non-optimal presentation and structure. There are also quite many
typos
-// The work presented in this paper, however, is still in a preliminary stage
- and convincing, novel scientific aspects are hardly identifiable
- (vedi sotto "Possibili spunti")
-
-/ include a short session on how you envision using the services from
- outside of H-Bugs, even outside of a proof-assistant environment if possible.
-/ how to integrate into H-Bugs for instance a computer algebra package as
- tutor for ring simplification or for computing witnesses
-/ the registration aspect seems quite different. In my understanding, this
- broker is a a very specialized planner in MONET terminology: it has internal
- knowledge of the domain area of proof assistants (it knows the formats of
- proof status and hints). The all architecture of H-Bugs has certain aspects
- that can be identified in the MONET architecture but it lacks the generality.
/ English: lots of errors in the third-person conjugation of verbs (missing s),
please correct them - I will not list all of them. Try to have a native
English speaker read the paper.
-/ Use Section instead of Sect.
- On receipt of an hint -> Upon receival of a hint
- An hint -> A hint (everywhere!)
- An usage -> A usage (check www.bartleby.com/64)
- reply the work -> replay/replicate? the work
-
-
-- About the broker, in w3c terminology one has connectors, components and
- gateways, wouldn't you say that the broker is a gateway?
-- You compare H-Bugs to the MONET architecture, why? Please shortly give a
- motivation. One may wonder why not comparing to Omega instead.
- Sessions 2 and 4 are too long, there are many repetitions.
-- Page 12: in the Calculemus tradition, intelligent tutors like CAS can be
- integrated with a skeptical approach. You must check former Calculemus
- proceedings for references.
+ROBA SOSTANZIALE:
-/ Page 9, do all tutors have the same interface? This is quite a uniform
- environment, which is not typical of a web service architecture. All the
- H-Bugs brokers provide a uniform H-Bugs broker interface.
-
-
-### (CRITICHE FEROCI)
-page 2: ... are natural candidates ...
-
-In MathWeb, for instance, many of the mentioned systems are not just
-candidates for being clients, they are clients.
-
-page 2: ... number of examples in the literature has been extremely low and
-the concrete benefits are still to be assessed.
-
-MathWeb, for instance, has been extensively used in case studies (where
-several thousands of subproblems have been attacked by MathWeb service
-systems).
-
-What is the novel aspect of your case study? What do I learn?
-
-page 2: The citation for MathWeb is not very well chosen. There is a system
-+description at CADE 2002 which is probably better suited. (This may also hold
-+for other citations.)
+// The work presented in this paper, however, is still in a preliminary stage
+ and convincing, novel scientific aspects are hardly identifiable
+ (vedi sotto "Possibili spunti")
Possibili spunti:
-(i) H-Bugs is an improved realization of the O-Ants approach; the
+NO: H-Bugs is an improved realization of the O-Ants approach; the
architecture of H-Bugs is superior to that of O-Ants and H-Bugs
provides more or at least some improved functionalities.
-(ii) H-Bugs is simply an adaptation of a subset of the functionalities
+YES: H-Bugs is simply an adaptation of a subset of the functionalities
of O-Ants to the MONET web-services/brokers approach.
-(iii) The paper presents a case study with H-Bugs that gives novel insights or
- provides new evidence for the usefulness of systems like H-Bugs and
+HHMM: The paper presents a case study with H-Bugs that gives novel insights or
+NO provides new evidence for the usefulness of systems like H-Bugs and
O-Ants. (Because the title says ...: a case study this is what the
reader first expects).
-(i) H-Bugs functionalities still appear to be a rather small subset of
- O-Ants functionalities. A proper comparison of functionalities is
- unfortunately missing. Example: H-Bugs does still present the
- hints in unsorted lists. Taking into account that the number of hints
- (especially when it comes to suggestions of parameters) can easily
- become very large, a heuristically structured presentation (which the
- authors mention as future work) seems to be a crucial requirement for
- such a system.
- There are many more aspects of O-Ants which seem to be not yet
- addressed in H-Bugs A proper comparison of the H-Bugs functionalities
- and architecture
- with the O-Ants functionalities and architecture should be given if the
- authors contribution is meant to be (i).
(ii) In the conclusion the authors admit that their work is rather
preliminary and that a real integration into the
MONET architecture is still missing. In addition the following critique
projects / helm.git / commitdiff