{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:53Z","timestamp":1725475793074},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_36","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"455-459","source":"Crossref","is-referenced-by-count":10,"title":["System Description: MBase, an Open Mathematical Knowledge Base"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Franke","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"Automated Deduction - CADE-14","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Ker-ber, M., Kohlhase, M., Konrad, K., Melis, E., Meier, A., Schaarschmidt, W., Siek-mann, J., Sorge, V.: \u03a9MEGA: Towards a mathematical assistant. In: CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 252\u2013255. Springer, Heidelberg (1997)"},{"key":"36_CR2","unstructured":"Caprotti, O., Cohen, A.M.: The Open Math standard. The Open Math Society (1998), http:\/\/www.nag.co.uk\/projects\/OpenHath\/omstd\/"},{"key":"36_CR3","volume-title":"Algebra Interactive!","author":"A. Cohen","year":"1999","unstructured":"Cohen, A., Cuypers, H., Sterk, H.: Algebra Interactive! Springer, Heidelberg (1999); Interactive Book on CD"},{"key":"36_CR4","unstructured":"Duchier, D.: The NEGRA tree bank. Private communication (1998)"},{"key":"36_CR5","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"Franke, A., Hess, S.M., Jung, C.G., Kohlhase, M., Sorge, V.: Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science\u00a05, 156\u2013187 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"36_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-48660-7_17","volume-title":"Automated Deduction - CADE-16","author":"A. Franke","year":"1999","unstructured":"Franke, A., Kohlhase, M.: System description: MATHWEB, an agent-based communication layer for distributed automated theorem proving. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 217\u2013221. Springer, Heidelberg (1999)"},{"key":"36_CR7","unstructured":"Hartmeier, M.: Aufbau einer Datenbank f\u00fcr mathematisclies Wissen. Master Thesis, Friedrich-Alexander-Universit\u00e4t Erlangen-Nurnberg (1997)"},{"key":"36_CR8","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/3-540-61511-3_92","volume-title":"Automated Deduction - Cade-13","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Sengler, C.: INKA - The Next Generation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 288\u2013292. Springer, Heidelberg (1996)"},{"key":"36_CR9","unstructured":"Hutter, D.: Reasoning about theories. Technical report, Deutsches Forscliungszentram f\u00fcr K\u00fcnstliche Intelligenz, DFKI (1999)"},{"key":"36_CR10","unstructured":"The isabelle online theory library. Internet interface at http:\/\/www4.informatik.tu-muenchen.de\/~isabelle\/library-1sabelie98-1"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Kohlhase, M., Franke, A.: 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":"36_CR12","unstructured":"Kohlhase, M.: OMDoc: Towards an OPENMATH representation of mathe\u00acmatical documents. Seki Report SR-00-02, Fachbereich Informatik, Universit\u00e4t des Saarlandes (2000), http:\/\/www.mathweb.org\/ilo\/omdoc"},{"key":"36_CR13","unstructured":"The Pvs libraries, http:\/\/pvs.csl.sri.com\/libraries.html"},{"key":"36_CR14","unstructured":"The QED manifesto (1995), Internet Report http:\/\/www.cybercom.net\/~rbjones\/rbjpub\/logic\/quedres00.htm"},{"key":"36_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BFb0015252","volume-title":"Computer Science Today","author":"G. Smolka","year":"1995","unstructured":"Smolka, G.: The Oz programming model. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 324\u2013343. Springer, Heidelberg (1995)"},{"key":"36_CR16","unstructured":"Stephen DeachExtensible stylesheet language (xsl) specification. W3c working draft, W3C (1999), Available at http:\/\/www.w3.org\/TR\/WD-xsl"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:38Z","timestamp":1556019758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/10721959_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}