Abstract
The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. By the application of XML technology to the large repositories of structured, content oriented information offered by Logical Frameworks we meet the ultimate goal of the Semantic Web, that is to allow machines the sharing and exploitation of knowledge in the Web way, i.e. without central authority, with few basic rules, in a scalable, adaptable, extensible manner.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I., “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.
Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I., “XML, Stylesheets and the re-mathematization of Formal Content”, Department of Computer Science, Bologna, Italy, May 2000.
Barras, et al., “The Coq Proof Assistant Reference Manual, version 6.3.1”, http://pauillac.inria.fr/coq/.
Coscoy, Y., Kahn, G., Thery, L., Extracting Text from Proofs. Technical Report RR-2459, INRIA Sophia Antipolis.
Coscoy, Y., “Explication textuelle de preuves pour le Calcul des Constructions Inductives”, Phd. Thesis, Université de Nice-Sophia Antipolis, 2000.
Berners-Lee, T., “Universal Resource Identifiers in WWW”, RFC 1630, CERN, June 1994.
Extensible Markup Language (XML) (Second Edition). Version 1.0. W3C Recommendation, 6 October 2000. http://www.w3.org/TR/REC-xml.
Mathematical Markup Language (MathML). Version 2.0. W3C Recommendation, 21 February 2001. http://www.w3.org/TR/MathML2/.
Namespaces in XML. W3C Recommendation, 14 January 1999. http://www.w3.org/TR/REC-xml-names/
Open Mathematical Documents (OMDoc) 1.0, November 1 2000. http://www.mathweb.org/omdoc/.
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/.
Simple Object Access Protocol (SOAP). Version 1.1. W3C Note, 8 May 2000. http://www.w3.org/TR/SOAP/.
XML Linking Language (XLink). Version 1.0. W3C Proposed Recommendation, 20 December 2000. http://www.w3.org/TR/xlink/.
XML Pointer Language (XPointer). Version 1.0. W3C Working Draft (Last Call), 8 January 2001. http://www.w3.org/TR/xptr/.
XML Path Language (XPath). Version 1.0, W3C Recommendation, 16 November 1999. http://www.w3.org/TR/xpath.
XSL Transformations (XSLT). Version 1.0, W3C Recommendation, 16 November 1999. http://www.w3.org/TR/xslt/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asperti, A., Padovani, L., Coen, C.S., Schena, I. (2001). HELM and the Semantic Math-Web. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_6
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive