{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T19:09:22Z","timestamp":1761764962990},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540420712"},{"type":"electronic","value":"9783540449904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44990-6_3","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T10:20:43Z","timestamp":1188296443000},"page":"32-52","source":"Crossref","is-referenced-by-count":21,"title":["OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge"],"prefix":"10.1007","author":[{"given":"Michael","family":"Kohlhase","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Towards an evolutionary formal software-development using CASL","author":"S. Autexier","year":"2000","unstructured":"Serge Autexier, Dieter Hutter, Heiko Mantel, and Axel Schairer. Towards an evolutionary formal software-development using CASL. In C. Choppy and D. Bert, editors, Proceedings Workshop on Algebraic Development Techniques, WADT-99. Springer, LNCS 1827, 2000."},{"key":"3_CR2","unstructured":"Alessandro Armando and Michael Kohlhase. Communication protocols for mathematical services based on KQML and OMRS. In Manfred Kerber and Michael Kohlhase, editors, CALCULEMUS-2000, Systems for Integrated Computation and Deduction, 2000, AKPeters."},{"key":"3_CR3","series-title":"Objectives of Open-Math","volume-title":"RIACA","author":"A. J. Abbot","year":"1996","unstructured":"[AvLS96] J. Abbot, A. van Leeuwen, and A. Strotmann. Objectives of Open-Math. Technical report 12, RIACA, Technische Universiteit Eindhoven, The Netherlands, June 1996."},{"key":"3_CR4","unstructured":"Alessandro Armando and Daniele Zini. Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture. In A. Poggi, editor, AI*IA-TABOO Workshop \u2018From Objects to Agents: Evolutionary Trends of Software Systems\u2019, 2000."},{"key":"3_CR5","unstructured":"Judith Baur. Syntax und semantik mathematisher texte\u2014ein prototyp. Master Thesis, Saarland University, 1999."},{"key":"3_CR6","unstructured":"Christoph Benzm\u00fcller, Matthew Bishop, and Volker Sorge. Integrating Tps and \u03a9mega. Journal of Universal Computer Science, 5(2), 1999."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"The \u03a9mega group. \u03a9mega: Towards a mathematical assistant. In William McCune, editor, CADE-14, LNAI 1249, pages 252\u2013255, 1997. Springer Verlag.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"3_CR8","unstructured":"Tim Bray, Jean Paoli, and C. M. Sperberg-McQueen. Extensible Markup Language (XML). W3C Recommendation TR-XML, December 1997. http:\/\/www.w3.org\/tr\/pr-xml.html ."},{"key":"3_CR9","unstructured":"Robert G. Bartle and Donald Sherbert. Introduction to Real Analysis. Wiley, 2 edition, 1982."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"R. Boulton, K. Slind, A. Bundy, and M. Gordon. An interface between CLAM and HOL. In Jim Grundy and Malcolm Newey, editors, TPHOLS-98, pages 87\u2013104, 1998.","DOI":"10.1007\/BFb0055131"},{"key":"3_CR11","unstructured":"Olga Caprotti and Arjeh M. Cohen. Draft of the OpenMath standard. The Open Math Society, http:\/\/www.nag.co.uk\/projects\/openmath\/omstd\/, 1998."},{"key":"3_CR12","unstructured":"Arjeh Cohen, Hans Cuypers, and Hans Sterk. Algebra Interactive! Springer Verlag, 1999. Interactive Book on CD."},{"key":"3_CR13","unstructured":"Language Design Task Group CoFI. Casl-the CoFI algebraic specification language-summary, version 1.0. Technical report, http:\/\/www.brics.dk\/projects\/cofi , 1998."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, and Tom Melham. The Prosper toolkit. In Proc. TACAS-2000, 2000.","DOI":"10.1007\/3-540-46419-0_7"},{"key":"3_CR15","unstructured":"Stephen Deach. Extensible stylesheet language (xsl) specification. W3c working draft, W3C, 1999. http:\/\/www.w3.org\/TR\/WD-xsl ."},{"key":"3_CR16","unstructured":"T. Finin and R. Fritzson. KQML\u2014a language and protocol for knowledge and information exchange. In Proceedings of the 13th Intl. Distributed Artificial Intelligence Workshop, pages 127\u2013136, 1994."},{"key":"3_CR17","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, and Volker Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 5:156\u2013187, 1999.","journal-title":"Journal of Universal Computer Science"},{"key":"3_CR18","unstructured":"Armin Fiedler. Towards a proof explainer. In Siekmann et al. [SPH97], pages 53\u201354."},{"key":"3_CR19","unstructured":"Armin Fiedler. Using a cognitive architecture to plan dialogs for the adaptive explanation of proofs. In Thomas Dean, editor, Proceedings IJCAI-99, pages 358\u2013363, 1999. Morgan Kaufmann."},{"key":"3_CR20","unstructured":"Andreas Franke and Michael Kohlhase. Communicating with MBASE in KQML. Internet Draft http:\/\/www.mathweb.org\/mbase , 1999."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Andreas Franke and Michael Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Harald Ganzinger, editor, Proceedings CADE-16, LNAI 1632, pages 217\u2013221. Springer Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_17"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Andreas Franke and Michael Kohlhase. System description: MBase, an open mathematical knowledge base. In David McAllester, editor, CADE-17, LNAI 1831, pages 455\u2013459. Springer Verlag, 2000.","DOI":"10.1007\/10721959_36"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Xiaorong Huang and Armin Fiedler. Presenting machine-found proofs. In M.A. McRobbie and J.K. Slaney, editors, Proceedings CADE-13, LNAI 1104, pages 221\u2013225, 1996. Springer Verlag.","DOI":"10.1007\/3-540-61511-3_83"},{"key":"3_CR24","unstructured":"Xiaorong Huang and Armin Fiedler. Proof verbalization in PROVERB. In Siekmann et al. [SPH97], pages 35\u201336."},{"key":"3_CR25","unstructured":"Helmut Horacek. Generating inference-rich discourse through revisions of RST-trees. In Proceedings AAAI-98, pages 814\u2013820. MIT Press, 1998."},{"key":"3_CR26","unstructured":"Dieter Hutter. Reasoning about theories. Technical report, DFKI, 1999."},{"key":"3_CR27","unstructured":"Patrick Ion and Robert Miner. Mathematical Markup Language (MathML) 1.0 specification. W3C Recommendation 1998. http:\/\/www.w3.org\/TR\/REC-MathML\/ ."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Michael Kohlhase and Andreas Franke. Mbase: Representing knowledge and context for the integration of mathematical software systems. Journal of Symbolic Comutation, 2000. forthcoming.","DOI":"10.1006\/jsco.2000.0468"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Michael Kohlhase. Creating omdoc representations from LATEX. Internet Draft http:\/\/www.mathweb.org\/omdoc , 2000.","DOI":"10.1145\/362001.362021"},{"key":"3_CR30","unstructured":"Michael Kohlhase. OMDoc: Towards an openmath representation of mathematical documents. Seki Report SR-00-02, Fachbereich Informatik, Universit\u00c4t des Saarlandes, 2000."},{"key":"3_CR31","unstructured":"William Mann and Sandra Thompson. Rhethorical structure theory: A theory of text organization. Technical Report ISI\/RR-83-115, ISI at University of Southern California, 1983."},{"key":"3_CR32","unstructured":"Dave Raggett, Arnaud Le Hors, and IanJacobs. HTML 4.0 Specification. W3C Recommendation 1998. http:\/\/www.w3.org\/TR\/PR-xml.html ."},{"key":"3_CR33","unstructured":"Martin Sch\u00f6nert et al. GAP\u2013Groups, Algorithms, and Programming. RWTH Aachen, Germany, 1995."},{"key":"3_CR34","unstructured":"[SBC+00] The \u03a9mega group. Adaptive course generation and presentation. In P. Brusilovski, editor, Proceedings of ITS-2000 workshop on Adaptive and Intelligent Web-Based Education Systems, Montreal, 2000."},{"key":"3_CR35","unstructured":"Y. Shoham. Agent-Oriented Programming. Technical report, Stanford University, 1990."},{"key":"3_CR36","unstructured":"M. Kohlhase S. Hess, Ch. Jung and V. Sorge. An implementation of distributed mathematical services. In Arjeh Cohen and Henk Barendregt, editors, CALCULEMUS and TYPES, 1998."},{"volume-title":"Proceedings of the First International Workshop on Proof Transformation and Presentation","year":"1997","key":"3_CR37","unstructured":"J. Siekmann, F. Pfenning, and X. Huang, editors. Proceedings of the First International Workshop on Proof Transformation and Presentation, Schloss Dagstuhl, Germany, 1997."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44990-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,26]],"date-time":"2020-04-26T01:12:15Z","timestamp":1587863535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44990-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540420712","9783540449904"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-44990-6_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}