From e0a70ebc4c3a81d1d6fb012ea39d856a6b89c032 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 23 May 2003 09:52:48 +0000 Subject: [PATCH] Minor improvements in the introduction. --- .../calculemus-2003/hbugs-calculemus-2003.tex | 50 ++++++++++--------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index f3fee9748..8c7252350 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -22,6 +22,8 @@ \newcommand{\wss}{Web-Services} \newcommand{\hbugs}{H-Bugs} \newcommand{\helm}{HELM} +\newcommand{\Omegapp}{$\Omega$mega} +\newcommand{\OmegaAnts}{$\Omega$mega-Ants} \title{Brokers and Web-Services for Automatic Deduction: a Case Study} @@ -59,10 +61,10 @@ \end{abstract} \section{Introduction} - The \ws\ approach at software development seems to be a working solution for + The \ws{} approach at software development seems to be a working solution for getting rid of a wide range of incompatibilities between communicating software applications. W3C's efforts in standardizing related technologies - grant longevity and implementations availability for frameworks based on \wss\ + grant longevity and implementations availability for frameworks based on \wss{}\ for information exchange. As a direct conseguence, the number of such frameworks is increasing and the World Wide Web is moving from a disorganized repository of human-understandable HTML documents to a disorganized repository @@ -76,10 +78,10 @@ This lack of organization along with the huge amount of documents available, have posed not a few problems for data location. If this limitation could be overcome using heuristic-based search engine for HTML pages, a satisfying - solution has yet to be found for \ws\ location \ednote{location non mi piace, ma + solution has yet to be found for \ws{} location \ednote{location non mi piace, ma "localization" e' anche peggio, "retrieval"?}. A promising architecture seems to be the use of \emph{brokers}, which access point (usually an URI) is known - by the potential clients or by \emph{registries}, to which the \wss\ subscribe + by the potential clients or by \emph{registries}, to which the \wss{} subscribe to publish their functionalities. } \begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale @@ -91,26 +93,26 @@ The standard solution is providing a further level of stable services applications to access a wide variety of services and abstract over them. Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET}, -following the guidelines of the \wss/brokers approach, is +following the guidelines of the \wss{}/brokers approach, is \end{newpart} working on the development of a framework aimed at providing a set of software tools for the advertisement and discovering of mathematical web services. -%CSC This framework turns out to be strongly based on both \wss\ and brokers. +%CSC This framework turns out to be strongly based on both \wss{} and brokers. \oldpart {Hhhmm. Chiaro il punto, ma CAS and Theorem Prover related web-services non \'e molto preciso.} { Several examples of CAS (Computer Algebra System) and Theorem Prover related - \wss\ have been shown to be useful and to fit well in the MONET Architecture + \wss{} have been shown to be useful and to fit well in the MONET Architecture \ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?} - the set of \wss\ related to Proof Assistants tends to be ... rather ... + the set of \wss{} related to Proof Assistants tends to be ... rather ... empty!\ednote{gia' mi immagino il tuo commento: BUHM! :-)} } \begin{newpart}{riformulo} - Several groups have already developed \wss\ providing both computational + Several groups have already developed \wss{} providing both computational and reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori - carini dalle conferenze calculemus}: the first ones are implemented - on top of Computer Algebra Systems; the last ones provide interfaces to + carini dalle conferenze calculemus}: the formers are implemented + on top of Computer Algebra Systems; the latters 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 services. Nevertheless, so far the number of examples in the @@ -119,42 +121,42 @@ following the guidelines of the \wss/brokers approach, is sodo prima che il lettore passi al caff\'e} \end{newpart} - In this paper we present an architecture, namely \hbugs\, implementing a + In this paper we present an architecture, namely \hbugs{}, implementing a \emph{suggestion engine} for the proof assistant developed on behalf of the - \helm\ project. We provide several \wss (called \emph{tutors}) able to + \helm{} project. We provide several \wss{} (called \emph{tutors}) able to suggest possible ways to proceed in a proof. The tutors are orchestrated - by a broker (a \ws\ itself) that is able to distribute a proof + by a broker (a \ws{} itself) that is able to distribute a proof status from a client (the proof-assistant) to the tutors; each tutor try to make progress in the proof and, in case - of success, notify the client that shows and \emph{hint} to the user. + of success, notify the client that shows an \emph{hint} to the user. Both the broker and the tutors are instances of the homonymous entities of the MONET framework. - A precursor of \hbugs is the $\Omega$-Ants project \cite{???}, + A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???}, which provided similar functionalities to the - Omega proof-planner \cite{Omega}. The main architectural difference - between \hbugs and $\Omega$-Ants is that the latter is based on a - black-board architecture and it is not implemented using \wss and + \Omegapp{} proof-planner \cite{Omega}. The main architectural difference + between \hbugs{} and \OmegaAnts{} is that the latter is based on a + black-board architecture and it is not implemented using \wss{} and brokers. Other differences will be detailed in Sect. \ref{conclusions}. - In Sect. \ref{architecture} we present the architecture of \hbugs. + 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. - Finally, the last section is left for the conclusions and future works. + As usual, the paper ends with the conclusions and future works. \oldpart {Non so se/dove mettere queste parti} { Despite of that the proof assistant case seems to be well suited to - investigate the usage of many different mathematical \wss. Indeed: most proof + investigate the usage of many different mathematical \wss{}. Indeed: most proof assistants are still based on non-client/server architectures, are application-centric instead of document-centric, offer a scarce level of automation leaving entirely to the user the choice of which macro (usually called \emph{tactic}) to use in order to make progress in a proof. - The average proof assistant can be, for example, a client of a \ws\ + The average proof assistant can be, for example, a client of a \ws{}\ interfacing a specific or generic purpose theorem prover, or a client of a - \ws\ interfacing a CAS to simplify expressions in a particular mathematical + \ws{} interfacing a CAS to simplify expressions in a particular mathematical domain. } -- 2.39.2