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.
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{???},
+ A precursor of \hbugs{} is the \OmegaAnts{} project \cite{omegaants},
which provided similar functionalities to the
- \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
+ \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}
\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
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
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{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{omegaants} 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.
\end{thebibliography}
projects / helm.git / commitdiff