X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Fhbugs-calculemus-2003.tex;h=24da5532dd3ca80f1e9732b41a3f6c4997059b6c;hb=ce6c4137bb0431c06df37d88e85a96807701e980;hp=ae81aba67494e65acd68b0d9a811deec74176f6c;hpb=b0d9f83fe0b38e6aa562998cf0c6053444541a91;p=helm.git diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index ae81aba67..24da5532d 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -29,7 +29,9 @@ \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\\ @@ -97,7 +99,7 @@ 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 @@ -123,6 +125,7 @@ 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. @@ -139,6 +142,14 @@ 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 @@ -147,11 +158,11 @@ 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{} @@ -212,6 +223,17 @@ 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. @@ -232,39 +254,40 @@ 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 @@ -275,15 +298,14 @@ to produce 23 hints. The first and not very useful hint suggests to proceed in 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 @@ -292,25 +314,26 @@ Double-clicking on the hint automatically applies 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 % @@ -379,7 +402,7 @@ the \hbugs{} architecture. 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 @@ -413,13 +436,14 @@ the \hbugs{} architecture. 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. @@ -484,7 +508,7 @@ the \hbugs{} architecture. 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. @@ -556,7 +580,7 @@ the \hbugs{} architecture. 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 @@ -705,6 +729,24 @@ we have investigated three classes of tutors: 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 @@ -757,7 +799,7 @@ we have investigated three classes of tutors: \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.\\ @@ -795,6 +837,10 @@ we have investigated three classes of tutors: 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} @@ -810,9 +856,10 @@ we have investigated three classes of tutors: \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.