From ae138b9558f6d0f2904b906aa08e633f56114fa7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 May 2003 17:51:48 +0000 Subject: [PATCH] - Introduction changed. - Tasks assigned. --- helm/papers/calculemus-2003/ed.sty | 13 +++ .../calculemus-2003/hbugs-calculemus-2003.tex | 80 ++++++++++++++----- helm/papers/calculemus-2003/outline.txt | 12 ++- 3 files changed, 83 insertions(+), 22 deletions(-) diff --git a/helm/papers/calculemus-2003/ed.sty b/helm/papers/calculemus-2003/ed.sty index 88e59df0b..aec692cc6 100644 --- a/helm/papers/calculemus-2003/ed.sty +++ b/helm/papers/calculemus-2003/ed.sty @@ -1,3 +1,9 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% 22/05/2003: New command 'oldpart' introduced by % +% Claudio Sacerdoti Coen % +% (a new environment would have been better) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Editorials % @@ -44,6 +50,13 @@ \def\tweak#1{\ifshowednotes\marginpar{{\sf tweak}(#1)}\fi} +\newcommand{\oldpart}[2]% motivation text +{\addtocounter{ednote}{1}\edef\new@number{\theednote}\message{Old Part!\new@number} +\ifshowednotes\ed@foot{#1}{Old Part}{}\marginpar{OldPart~Missing(\new@number)}\fi} + +\def\ednotemessage{\ifnum\value{ednote}>0\typeout{}% +\typeout{There are still \arabic{ednote} EdNotes and Issues to resolve!}% +\typeout{}\fi} \def\df#1{\bf{#1}} \def\dfi#1{\bf{\index*{#1}}} diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index feefda5cc..f3fee9748 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -64,11 +64,15 @@ software applications. W3C's efforts in standardizing related technologies grant longevity and implementations availability for frameworks based on \wss\ for information exchange. As a direct conseguence, the number of such - frameworks in increasing and the World Wide Web is moving from a disorganized + frameworks is increasing and the World Wide Web is moving from a disorganized repository of human-understandable HTML documents to a disorganized repository of applications working on machine-understandable XML documents both for input and output. +\oldpart +{Di effetto la prima fase. La seconda era troppo fuori-tema e dettagliata per + un abstract} +{ 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 @@ -77,18 +81,70 @@ 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 to publish their functionalities. +} +\begin{newpart}{Questa \'e la mia contro-proposta. Nella mia idea originale +dovrebbe essere una versione pi\'u fluida e leggera. Boh.} +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 for client +applications to access a wide variety of services and abstract over them. - Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET} is +Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET}, +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. This - framework turns out to be strongly based on both \wss\ and brokers. - + tools for the advertisement and discovering of mathematical web services. +%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 \ednote{citarne qualcuno: CSC???}. On the other hand \ednote{troppo informale?} 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 + 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 + 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 + literature has been extremely low and the concrete benefits are still + to be assessed.\ednote{A questo punto bisogna venire al + sodo prima che il lettore passi al caff\'e} +\end{newpart} + + 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 + 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 + 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. + 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{???}, + 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 + brokers. Other differences will be detailed in Sect. \ref{conclusions}. + + 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. + +\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 assistants are still based on non-client/server architectures, are @@ -100,20 +156,8 @@ interfacing a specific or generic purpose theorem prover, or a client of a \ws\ interfacing a CAS to simplify expressions in a particular mathematical domain. +} - The Omega Ants project \ednote{date, autori e paperi}, developed before the - \emph{\ws\ era}, enrich the Omega \cite{Omega} proof assistant with an - architecture able to distribute subparts of a proof to agents (Ants) - implemented as separate processes running on the same hosts of the proof - assistant \ednote{controllare ...}. - - 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. This architecture is based on a set of \wss\ and a broker (a - \ws\ itself) and is able to distribute a proof status from a client to several - \emph{tutor}, each of them can try to make progress in the proof and, in case - of success, notify the user sending him an \emph{hint}. Both the broker and - the tutors are instances of the homonymous entities of the MONET framework. % \section{Introduction} % Since the development of the first proof-assistants based on the diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt index d349353fa..138f3b719 100644 --- a/helm/papers/calculemus-2003/outline.txt +++ b/helm/papers/calculemus-2003/outline.txt @@ -1,4 +1,5 @@ -1) Introduzione +1) Zack, CSC + Introduzione - web services - monet - svariati WS per CAS e TP @@ -7,7 +8,8 @@ - application centric no client/server ==>> proof assistants come WS client - omega ants -2) Architettura +2) Zack + Architettura - figura 7.1 mia tesi - attori (client, broker, tutor) - ruoli e funzionalita' di ognuno di essi (breve) @@ -29,9 +31,11 @@ - nessuna assunzione sulla correttezza del suggerimento - interfaccia verso il broker (start/stop musing) - thread (?) -4) Sample session +4) CSC + Sample session - screen shot -5) Tutor implementati +5) CSC + Tutor implementati - stupidi - (1-1) con le tattiche del proof assistant - generazione automatica -- 2.39.2