From 19659c576c72bdb11eec1cead45de3f2d19a83d7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 29 May 2003 21:14:06 +0000 Subject: [PATCH] draft review --- .../calculemus-2003/hbugs-calculemus-2003.tex | 49 +++++++++++-------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index f0165276c..b91c1ef52 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -51,9 +51,9 @@ \begin{abstract} We present a planning broker and several Web-Services for automatic deduction. - Each Web-Service implements one of the tactics usually available in an - interactive proof-assistant. When the broker is submitted a "proof status" (an - unfinished proof tree and a focus on an open goal) it dispatches the proof to + Each Web-Service implements one of the tactics usually available in + interactive proof-assistants. When the broker is submitted a "proof status" (an + incomplete proof tree and a focus on an open goal) it dispatches the proof to the Web-Services, collects the successful results, and send them back to the client as "hints" as soon as they are available. @@ -75,8 +75,8 @@ 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 is providing a further level of - stable services (called \emph{brokers}) that behave as common gateway/address + The standard solution is to provide a further level of + stable services (called \emph{brokers}) that behave as common gateways/addresses for client applications to access a wide variety of services and abstract over them. @@ -95,7 +95,7 @@ Computer Algebra Systems; the second ones provide interfaces to well-known theorem provers. Proof-planners, proof-assistants, CAS and - domain-specific problem solvers are natural candidates to be client of these + 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. @@ -110,7 +110,7 @@ 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. The broker is an instance of the homonymous entity of the MONET framework. - The tutors are MONET services. Another \ws (which is not described in this + The tutors are MONET services. Another \ws{} (which is not described in this paper and which is called Getter \cite{zack}) is used to locate and download mathematical entities; the Getter plays the role of the Mathematical Object Manager in the MONET framework. @@ -125,7 +125,7 @@ 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. + As usual, the final section of this paper is devoted to conclusions and future works. \section{An \hbugs{} Bird's Eye View} \label{architecture} @@ -136,7 +136,7 @@ Each actor present one or more \ws{} interfaces to its neighbors \hbugs{} actors. - In this section we will detail the role and requirements of each kind of + 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}. @@ -180,7 +180,7 @@ mathematical items in the \helm{} library. The proof status that are exchanged by the \hbugs{} actors, instead, are built on the fly and are neither - stored nor are given an unique identifier (URI) to be managed by the + stored nor given an unique identifier (URI) to be managed by the Getter. \paragraph{Brokers} @@ -229,11 +229,12 @@ etc.). The only requirement is that there exists an agreement on the formats of proof status and hints. - Tutors act both as \ws{} providers and requesters for the broker. As + Tutors act both as \ws{} providers and requesters for the broker, see Fig. + \ref{interfaces}. 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). + outcome (an hint in case of success or a failure notification). \hbugs{} tutors act as MONET services. @@ -275,7 +276,7 @@ the \hbugs{} architecture. In order to complete the proof, the user has to instantiate every metavariable in the proof with a proof of the corresponding goal. Each goal is identified by an unique identifier and has a context - and a type ( the goal thesis). The context is a list of named + and a type (the goal thesis). The context is a list of named hypotheses (declarations and definitions). Thus the context and the goal thesis form a sequent, which is the statement of the proof that will be used to instantiate the metavariable occurrences. @@ -333,6 +334,8 @@ the \hbugs{} architecture. 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. + \ednote{Zack: che ne dici di un "reinvent the whell" qui sopra? fa sempre + effetto ...} An alternative implementation where the tutors are trusted would simply send back to the client a new proof-status. Upon receiving the @@ -371,14 +374,16 @@ the \hbugs{} architecture. \ws{}. Additionally tutors are required to send an human readable description of their capabilities; this information could be used by client's user to - decide which tutors he needs to subscribe to. Like clients, tutors can + decide which tutors he needs to subscribe to. Like clients\ednote{Zack: mi + pare che questo sia un caso in cui si debba usare "as" e non like, ma non ne + sono certo}, tutors can unregister from brokers using \texttt{Unregister\_broker} method. - Each time the client status change, the status is sent to the + Each time the client status change, it get sent sent to the broker using its \texttt{Status} method. Using both clients registry (to lookup client's subscription) and tutors registry (to check if some tutors has unsubscribed), the broker is able to decide to which tutors the - new status must be forwarded.\ednote{CSC: qui o nei lavori futuri parlare + new status have to be forwarded.\ednote{CSC: qui o nei lavori futuri parlare della possibilit\'a di avere un vero brocker che multiplexi le richieste dei client localizzando i servizi, etc.} @@ -516,6 +521,8 @@ we have investigated three classes of tutors: of $n \le n$ is simply the application of the first constructor to $n$ and a proof of $n \le m$ is the application of the second constructor to $n,m$ and a proof of $n \le m$.}. + \ednote{Zack: non e' necessario specificare che stai parlando di numeri + naturali nella footnote?} Since disjunction, conjunction, existential quantification and Leibniz equality are particular cases of inductive propositions, all the other tutors of this class are instantiations of the @@ -581,7 +588,7 @@ we have investigated three classes of tutors: To test the productivity impact of intelligent tutors, we have implemented a tutor that is interfaced with the \helm{} - Search-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that + Search-Engine\footnote{\url{http://helm.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 @@ -657,7 +664,7 @@ we have investigated three classes of tutors: To conclude, \hbugs{} is a nice experiment meant to understand whether the current \wss{} technology is mature enough to have a concrete and useful - impact on the daily work of users of proof-assistants. So far, only the tutor + impact on the daily work of proof-assistants users. So far, only the tutor that is interfaced with the \helm{} Search-Engine has effectively increased the productivity of experts users. The usefulness of the tutors developed for beginners, instead, need further assessment. @@ -675,7 +682,7 @@ we have investigated three classes of tutors: Deduction Systems via the Logic Broker Architecture. In Proceedings of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000. -\bibitem{ws3} O. Caprotti. Symbolic Evaluator Service. Project Report of +\bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz, Austria, May 2002. @@ -718,11 +725,11 @@ 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{ws4} J. Zimmer and L. Dennis. Inductive Theorem Proving and +\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{ws2} R. Zippel. The MathBus. In Workshop on Internet Accessible +\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999. \end{thebibliography} -- 2.39.2