Abstract
The paper describes the general philosophy and the main architectural and technological solutions adopted in the HELM Project for the management of large repositories of mathematical knowledge. The leitmotiv is the extensive use of XML technology, and the exploitation of information in the “Web way”, that is without a central authority, with few basic rules, in a scalable, adaptable, and extensible manner.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Document Object Model (DOM) Level 2 Core Specification. Version 1.0, W3C Recommendation (13 November 2000). http://www.w3.org/TR/2000/REC-DOM-Level-2-Core-20001113/.
ExtensibleMarkup Language (XML) Specification. Version 1.0.W3C Recommendation (10 February 1998). http://www.w3.org/TR/REC-xml.
Mathematical Markup Language (MathML) 2.0 W3C Recommendation (21 February 2001). http://www.w3.org/TR/MathML2/.
Resource Description Framework (RDF) Model and Syntax Specification, W3C Recommendation (22 February 1999). http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/.
Resource Description Framework (RDF) Schema Specification 1.0, W3C Candidate Recommendation (27 March 2000). http://www.w3.org/TR/rdf-schema/.
XML Linking Language (XLink), W3C Working Draft (last call) (21 February 2000). http://www.w3.org/TR/xlink/.
XSL Transformations (XSLT). Version 1.0, W3C Recommendation (16 November 1999). http://www.w3.org/TR/xslt.
XQuery 1.0: An XML Query Language, W3C Working Draft (30 April 2002). http://www.w3.org/TR/xquery/.
A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, Content-centric logical environments, short presentation at LICS'2000, Santa Barbara, CA (June 26–28, 2000).
A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, Formal mathematics in MathML, in: Proceedings of the First International Conference on MathML and Math on the Web, University of Illinois at Urbana-Champaign (October 20–21, 2000).
A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, Formal mathematics on the Web, in: Proceedings of the Eighth International Conference on Libraries and Associations in the Transient World: New Technologies and New Forms of Cooperation, Sudak, Autonomous Republic of Crimea, Ukraine (June 9–17, 2001).
A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, XML, Stylesheets and the remathematization of Formal Content, in: Proceedings of Extreme Markup Languages 2001 Conference, Montréal, Canada (August 12–17, 2001).
A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, HELM and the semantic Math-Web, in: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2001), Edinburgh, Scotland, 3–6 September 2001.
B. Barras et al., The Coq Proof Assistant Reference Manual, Version 6.3.1, http://pauillac.inria.fr/coq.
O. Caprotti, H. Geuvers and M. Oostdijk, Certified and Portable mathematical documents from formal contexts, in: Proceedings of the First International Workshop on Mathematical Knowledge Management, September 2001.
P. Casarini and L. Padovani, The Gnome DOM Engine, acepted paper at the Extreme Markup Language 2001 Conference, August 2001.
R. Constable et al. Implementing Mathematics with the Nuprl Development System (Prentice-Hall, Englewood Cliffs, NJ, 1986).
Y. Coscoy, G. Kahn and L. Thery, Extracting text from proofs, Technical Report RR-2459, INRIA Sophia Antipolis.
Y. Coscoy, Explication textuelle de preuves pour le Calcul des Constructions Inductives, Ph.D. Thesis, Université de Nice-Sophia Antipolis (2000).
G. Huet and G. Plotkin, eds., Logical Frameworks (Cambridge University Press, Cambridge, MA, 1991).
G. Huet and G. Plotkin, eds., Logical Environments (Cambridge University Press, Cambridge, MA, 1993).
J. Kahan, M. Koivunen, E. Prud'Hommeaux and R.R. Swick, Annotea: An open RDF infrastructure for shared Web annotations, in: Proc. of the WWW10 International Conference, Hong Kong (May 2001).
M. Kohlase, OMDoc: Towards an OpenMath representation of mathematical documents, Technical Report, http://www.mathweb.org/omdoc/index.html.
M. Kohlase, OMDoc: Towards an Internet standard for the administration, distribution and teaching of mathematical knowledge, in: Proceedings of Conf. on Artificial Intelligence and Symbolic Computation, Lecture Notes in Artificial Intelligence (Springer, Berlin, 2000).
M. Kohlase, OMDoc: An infrastructure for OpenMath Content dictionary information, Bulletin of the ACM Special Interest Group for Algorithmic Mathematics SIGSAM (2000).
B. Naylor and S. Watt, Meta style sheets for the conversion of mathematical documents into multiple forms, in: On-line Proceedings of the First International Workshop on Mathematical Knowledge Management (2001).
M. Oostdijk, Generation and presentation of formal mathematical documents, Ph.D. Thesis, University of Eindhoven.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Asperti, A., Padovani, L., Sacerdoti Coen, C. et al. Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence 38, 27–46 (2003). https://doi.org/10.1023/A:1022907629104
Issue Date:
DOI: https://doi.org/10.1023/A:1022907629104