{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T03:07:23Z","timestamp":1762916843435,"version":"3.40.5"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1023\/a:1022907629104","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T22:16:51Z","timestamp":1049753811000},"page":"27-46","source":"Crossref","is-referenced-by-count":33,"title":["Mathematical Knowledge Management in HELM"],"prefix":"10.1007","volume":"38","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferruccio","family":"Guidi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Irene","family":"Schena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5118018_CR1","unstructured":"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\/."},{"key":"5118018_CR2","unstructured":"ExtensibleMarkup Language (XML) Specification. Version 1.0.W3C Recommendation (10 February 1998). http:\/\/www.w3.org\/TR\/REC-xml."},{"key":"5118018_CR3","unstructured":"Mathematical Markup Language (MathML) 2.0 W3C Recommendation (21 February 2001). http:\/\/www.w3.org\/TR\/MathML2\/."},{"key":"5118018_CR4","unstructured":"Resource Description Framework (RDF) Model and Syntax Specification, W3C Recommendation (22 February 1999). http:\/\/www.w3.org\/TR\/1999\/REC-rdf-syntax-19990222\/."},{"key":"5118018_CR5","unstructured":"Resource Description Framework (RDF) Schema Specification 1.0, W3C Candidate Recommendation (27 March 2000). http:\/\/www.w3.org\/TR\/rdf-schema\/."},{"key":"5118018_CR6","unstructured":"XML Linking Language (XLink), W3C Working Draft (last call) (21 February 2000). http:\/\/www.w3.org\/TR\/xlink\/."},{"key":"5118018_CR7","unstructured":"XSL Transformations (XSLT). Version 1.0, W3C Recommendation (16 November 1999). http:\/\/www.w3.org\/TR\/xslt."},{"key":"5118018_CR8","unstructured":"XQuery 1.0: An XML Query Language, W3C Working Draft (30 April 2002). http:\/\/www.w3.org\/TR\/xquery\/."},{"key":"5118018_CR9","unstructured":"A. Asperti, L. Padovani, C. Sacerdoti Coen and I. Schena, Content-centric logical environments, short presentation at LICS'2000, Santa Barbara, CA (June 26\u201328, 2000)."},{"key":"5118018_CR10","volume-title":"Proceedings of the First International Conference on MathML and Math on the Web","author":"A. Asperti","year":"2000","unstructured":"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\u201321, 2000)."},{"key":"5118018_CR11","unstructured":"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\u201317, 2001)."},{"key":"5118018_CR12","unstructured":"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\u00e9al, Canada (August 12\u201317, 2001)."},{"key":"5118018_CR13","doi-asserted-by":"crossref","unstructured":"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\u20136 September 2001.","DOI":"10.1007\/3-540-44755-5_6"},{"key":"5118018_CR14","unstructured":"B. Barras et al., The Coq Proof Assistant Reference Manual, Version 6.3.1, http:\/\/pauillac.inria.fr\/coq."},{"key":"5118018_CR15","unstructured":"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."},{"key":"5118018_CR16","doi-asserted-by":"crossref","unstructured":"P. Casarini and L. Padovani, The Gnome DOM Engine, acepted paper at the Extreme Markup Language 2001 Conference, August 2001.","DOI":"10.1162\/109966201317356399"},{"key":"5118018_CR17","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. Constable","year":"1986","unstructured":"R. Constable et al. Implementing Mathematics with the Nuprl Development System (Prentice-Hall, Englewood Cliffs, NJ, 1986)."},{"key":"5118018_CR18","unstructured":"Y. Coscoy, G. Kahn and L. Thery, Extracting text from proofs, Technical Report RR-2459, INRIA Sophia Antipolis."},{"key":"5118018_CR19","volume-title":"Explication textuelle de preuves pour le Calcul des Constructions Inductives","author":"Y. Coscoy","year":"2000","unstructured":"Y. Coscoy, Explication textuelle de preuves pour le Calcul des Constructions Inductives, Ph.D. Thesis, Universit\u00e9 de Nice-Sophia Antipolis (2000)."},{"volume-title":"Logical Frameworks","year":"1991","key":"5118018_CR20","unstructured":"G. Huet and G. Plotkin, eds., Logical Frameworks (Cambridge University Press, Cambridge, MA, 1991)."},{"volume-title":"Logical Environments","year":"1993","key":"5118018_CR21","unstructured":"G. Huet and G. Plotkin, eds., Logical Environments (Cambridge University Press, Cambridge, MA, 1993)."},{"key":"5118018_CR22","doi-asserted-by":"crossref","unstructured":"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).","DOI":"10.1145\/371920.372166"},{"key":"5118018_CR23","unstructured":"M. Kohlase, OMDoc: Towards an OpenMath representation of mathematical documents, Technical Report, http:\/\/www.mathweb.org\/omdoc\/index.html."},{"key":"5118018_CR24","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of Conf. on Artificial Intelligence and Symbolic Computation","author":"M. Kohlase","year":"2000","unstructured":"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)."},{"key":"5118018_CR25","doi-asserted-by":"crossref","unstructured":"M. Kohlase, OMDoc: An infrastructure for OpenMath Content dictionary information, Bulletin of the ACM Special Interest Group for Algorithmic Mathematics SIGSAM (2000).","DOI":"10.1145\/362001.362021"},{"key":"5118018_CR26","unstructured":"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)."},{"key":"5118018_CR27","unstructured":"M. Oostdijk, Generation and presentation of formal mathematical documents, Ph.D. Thesis, University of Eindhoven."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022907629104.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022907629104\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022907629104.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:41Z","timestamp":1747546961000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022907629104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":27,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["5118018"],"URL":"https:\/\/doi.org\/10.1023\/a:1022907629104","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}