From 0b623a013a3550871893aa8960a176ec234da5e7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 May 2003 12:22:28 +0000 Subject: [PATCH] Many references committed. --- .../calculemus-2003/hbugs-calculemus-2003.tex | 100 +++++++++--------- 1 file changed, 50 insertions(+), 50 deletions(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 1ec47373f..66ada2b98 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -80,8 +80,9 @@ 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. @@ -107,13 +108,13 @@ 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} @@ -301,7 +302,7 @@ 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 @@ -432,7 +433,7 @@ the \hbugs{} architecture. 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 @@ -577,7 +578,7 @@ we have investigated three classes of tutors: 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, @@ -626,7 +627,7 @@ we have investigated three classes of tutors: 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 @@ -684,47 +685,46 @@ we have investigated three classes of tutors: \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} -- 2.39.2