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 working on the development of a framework, based on the
+ Since the \emph{Declaration of Linz}, the MONET
+ Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}}
+ is working on the development of a framework, based on the
\wss{}/brokers approach, aimed at providing a set of software tools for the
advertisement and the discovery of mathematical \wss{}.
%CSC This framework turns out to be strongly based on both \wss{} and brokers.
- Several groups have already developed \wss{} providing both computational and
- reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
- dalle conferenze calculemus}: the formers are implemented on top of
+ Several groups have already developed software bus and
+ services\footnote{The most part of these systems predate the development of
+ \wss. Those systems whose development is still active are slowly being
+ reimplemented as \wss.} providing both computational and reasoning
+ capabilities \cite{ws1,ws2,ws3,ws4}: 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
+ 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.
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
- paper and which is called Getter \cite{}) is used to locate and download
+ 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.
- A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
- which provided similar functionalities to the
- \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
+ A precursor of \hbugs{} is the \OmegaAnts{} project
+ \cite{omegaants1,omegaants2}, which provided similar functionalities to the
+ \Omegapp{} proof-planner \cite{omega}. The main architectural difference
between \hbugs{} and \OmegaAnts{} are 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}
Sect. \ref{tutors} is an overview of the tutors that have been implemented.
As usual, the paper ends with the conclusions and future works.
-\oldpart
-{CSC: Non so se/dove mettere queste parti.
- Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
- non e' molto utile, ma la seconda sugli usi tipici di proof assistant
- come ws client si}
-{
- 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
- 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{}\
- 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.
-}
-
-\section{An \hbugs{} Bird'S Eye View\ednote{Zack: sono in vena di boiate
-stasera!}}
+\section{An \hbugs{} Bird'S Eye View}
\label{architecture}
\myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
\wss{} interfaces}
Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
- providers and requesters, see \ednote{Zack: va bene "see"?, "cfr" credo sia
- solo italiano ...} Fig. \ref{interfaces}.
+ providers and requesters, see Fig. \ref{interfaces}.
They act as providers for the broker (to receive hints)
and as requesters (to submit new status). Clients
additionally use broker service to know which tutors are available and to
\section{Implementation's Highlights}
\label{implementation}
-\ednote{Zack: l'aspetto grafico di questa parte e' un po' peso, possiamo
-aggiungere varie immagini volendo, e.g.: schema dei thread di un tutor, sample
-code di un tutor generato automaticamente}
In this section we present some of the most relevant implementation details of
the \hbugs{} architecture.
\end{description}
Each of these information is represented in XML as described in
- \cite{csc-thesis}. Additionally, an \hbugs{} status carry the unique
+ \cite{mowglicic}. Additionally, an \hbugs{} status carry the unique
identifier of the current goal, which is the goal the user is currently
focused on. Using this value it is possible to implement different client
side strategies: the user could ask the tutors to work on the goal
broker to send him an unique identifier and its base URI as a
\ws{}. After the registration, the client can use broker's
\texttt{List\_tutors} method to get a list of available tutors.
- Eventually\ednote{CSC: Vuoi veramente dire eventually qui? Zack: si, prima o
- poi lo faranno ...} the
- client can subscribe to one or more of these using broker's
+ Eventually the client can subscribe to one or more of these using broker's
\texttt{Subscribe} method. Clients can also unregister from brokers using
\texttt{Unregister\_client} method.
Consulting the \musings{} registry, the tutor\ednote{CSC: ma \'e vero o
stai delirando? Zack: e' vero, non ti fidi? :-) Up to delay di rete
- ovviamente ...} is able to know, at each time,
+ ovviamente ... CSC: ma a che serve???} is able to know, at each time,
which \musings{} are in execution on which tutor. This peculiarity is
exploited by the broker on invocation of Status method. Receiving a new
status from the client implies indeed that the previous status no longer
As already discussed, all \hbugs{} actors act as \wss{} offering one or more
services to neighbour actors. To grant as most accessibility as possible to
our \wss{} we have chosen to bind them using the HTTP/POST bindings
- described in \cite{????}\footnote{Given that our proof assistant was
+ described in \cite{wsdlbindings}\footnote{Given that our proof assistant was
entirely developed in the Objective Caml language, we have chosen to
develop also \hbugs{} in that language in order to maximize code reuse. To
develop \wss{} in Objective Caml we have developed an auxiliary generic
resources.\ednote{CSC: A cosa dobbiamo questa architettura delirante? Se non
ricordo male al problema dell'uccisione dei thread. Ora o si spiega
il motivo di questa architettura o si glissa/bluffa. Zack: cosa ti sembra
- delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...}
+ delirante? che i thread vengono uccisi? ... non mi e' molto chiaro ...
+ CSC: la motivazione per avere due thread always running e non due}
This architecture turns out to be scalable and allows the running threads
to share the cache of loaded (and type-checked) theorems.
can easily pre-load the required theorems.
As an example of computationally expensive task, we have implemented
- a tutor for the \emph{Ring} tactic \cite{ring_bouting}.
+ a tutor for the \emph{Ring} tactic \cite{ringboutin}.
The tutor is able to prove an equality over a ring by reducing both members
to a common normal form. The reduction, which may require some time in
complex cases,
for Mathematical \wss{}.
A running prototype has been implemented as part of the
- \helm{} project \cite{}
+ \helm{} project \cite{helm}
and we already provide several tutors. Some of them are simple tutors that
try to apply one or more tactics of the \helm{} Proof-Engine, which is also
our client. We also have a much more complex tutor that is interfaced
\begin{thebibliography}{01}
-% \bibitem{ALF} The ALF family of proof-assistants:\\
-% {\tt http://www.cs.chalmers.se/ComputingScience/Research/\\Logic/implementation.mhtml}
-%
-% \bibitem{Coq} The Coq proof-assistant:\\
-% {\tt http://coq.inria.fr/}
-%
-% \bibitem{FORMAVIE} The Formavie project:\\
-% {\tt http://http://www-sop.inria.fr/oasis/Formavie/}
-%
-% \bibitem{EHELM} The HELM project:\\
-% {\tt http://www.cs.unibo.it/helm/}
-%
-% \bibitem{MATHWEB} The MathWeb project:\\
-% {\tt http://www.mathweb.org/}
-%
-% \bibitem{PCOQ} The PCoq project:\\
-% {\tt http://www-sop.inria.fr/lemme/pcoq/}
-%
-% \bibitem{HELM} A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
-% Towards a library of formal mathematics. Panel session of
-% the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLS'2000),
-% Portland, Oregon, USA.
-%
-% \bibitem{Ring} S. Boutin. Using reflection to build efficient and certified
-% decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS'97,
-% volume 1281. LNCS, Springer-Verlag, 1997.
-%
-% \bibitem{YANNTHESIS} Y.Coscoy. \emph{Explication textuelle de preuves pour le
-% Calcul des Constructions Inductives}, PhD. Thesis, Universit\'e de Nice-Sophia
-% Antipolis, 2000.
-%
-% \bibitem{ALFA} T. Hallgreen, Aarne Ranta. An Extensible Proof Text Editor.
-% Presented at LPAR2000.
-%
-% \bibitem{Necula} G. Necula, P. Lee. Safe Kernel Extensions Without Run-Time
-% Checking. Presented at OSDI'96, October 1996.
-%
-% \bibitem{Necula2} G. Necula, P. Lee. Efficient Representation and Validation of Proofs. Presented at LICS'98, June 1998
-%
-% \bibitem{Werner} B. Werner. \emph{Une Th\'eorie des Constructions Inductives},
-% PhD. Thesis, Universit\'e Paris VII, May 1994.
+\bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
+ \url{http://www.w3.org/TR/ws-gloss/}
+
+\bibitem{wsdlbindings} Web Services Description Language (WSDL)
+ Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
+ \url{http://www.w3.org/TR/wsdl12-bindings/}
+
+\bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
+ 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
+ the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
+ Austria, May 2002.
+
+\bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
+ Mathematical Knowledge Management in HELM. In Annals of Mathematics and
+ Artificial Intelligence, 38(1): 27--46, May 2003.
+
+\bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
+ at Combining Interactive and Automated Theorem Proving. In M. Kerber and
+ M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
+ 81--97, 2000.
+
+\bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
+ Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
+ Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
+
+\bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler,
+ X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier,
+ W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical
+ Assistant. In W. McCune (ed), Proceedings of the 14th Conference on
+ Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255,
+ Townsville, Australia, 1997.
+
+\bibitem{ringboutin} S. Boutin. Using reflection to build efficient and
+ certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
+ TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
+
+\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{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable
+ D2.a.\\
+ \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html}
+
+\bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the
+ Bad Habit of Overkilling. In Supplementary Proceedings of the 14th
+ International Conference TPHOLS 2001, pp. 352--367, Edinburgh.
+
+\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
+ 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
+ Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
\end{thebibliography}
projects / helm.git / blobdiff