{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T05:16:59Z","timestamp":1774588619281,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642026133","type":"print"},{"value":"9783642026140","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_21","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T11:47:24Z","timestamp":1246535244000},"page":"233-246","source":"Crossref","is-referenced-by-count":14,"title":["A Review of Mathematical Knowledge Management"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Carette","sequence":"first","affiliation":[]},{"given":"William M.","family":"Farmer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Adams, A.A.: Digitisation, representation, and formalisation. In: Asperti, et al. (eds.) [4], pp. 1\u201316","DOI":"10.1007\/3-540-36469-2_1"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Adams, A.A., Davenport, J.H.: Copyright issues for MKM. In: Asperti, et al. (eds.) [3], pp. 1\u201316","DOI":"10.1007\/978-3-540-27818-4_1"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Knowledge Management","year":"2004","unstructured":"Asperti, A., Bancerek, G., Trybulec, A. (eds.): MKM 2004. LNCS, vol.\u00a03119. Springer, Heidelberg (2004)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Knowledge Management","year":"2003","unstructured":"Asperti, A., Buchberger, B., Davenport, J.H. (eds.): MKM 2003. LNCS, vol.\u00a02594. Springer, Heidelberg (2003)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. In: Kauers, et al. (eds.) [27], pp. 161\u2013175","DOI":"10.1007\/978-3-540-73086-6_15"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Intelligent Computer Mathematics","year":"2008","unstructured":"Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.): AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol.\u00a05144. Springer, Heidelberg (2008)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Knowledge Management","year":"2006","unstructured":"Borwein, J.M., Farmer, W.M. (eds.): MKM 2006. LNCS, vol.\u00a04108. Springer, Heidelberg (2006)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Borwein, J.M., Stanway, T.: Managing digital mathematical discourse. In: Asperti, et al. (eds.) [4], pp. 45\u201355","DOI":"10.1007\/3-540-36469-2_4"},{"key":"21_CR9","unstructured":"Boyer, R.: The QED Manifesto. In: Bundy, A. (ed.) Proceedings CADE 12, pp. 238\u2013251 (1994)"},{"key":"21_CR10","unstructured":"Buchberger, B., Caprotti, O. (eds.): Electronic Proceedings of the First International Workshop on Mathematical Knowledge Management: MKM 2001. RISC-Linz (2001), http:\/\/www.risc.uni-linz.ac.at\/about\/conferences\/MKM2001\/Proceedings"},{"key":"21_CR11","series-title":"Ann. Math. Artif. Intell","volume-title":"Mathematical Knowledge Management","year":"2003","unstructured":"Buchberger, B., Gonnet, G.H., Hazewinkel, M. (eds.): Mathematical Knowledge Management. Ann. Math. Artif. Intell, vol.\u00a038. Kluwer, Dordrecht (2003)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Bundy, A.: Automating signature evolution in logical theories. In: Autexier, et al. (eds.) [6], pp. 333\u2013338","DOI":"10.1007\/978-3-540-85110-3_29"},{"issue":"1-3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1022963714083","volume":"38","author":"P.A. Cairns","year":"2003","unstructured":"Cairns, P.A., Gow, J., Collins, P.: On dynamically presenting a topology course. Ann. Math. Artif. Intell.\u00a038(1-3), 91\u2013104 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"21_CR14","unstructured":"Cajori, F.: A History of Mathematical Notations. Dover, New York (reprint) (1929)"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Coen, C.S.: From proof-assistants to distributed libraries of mathematics: Tips and pitfalls. In: Asperti, et al. (eds.) [4], pp. 30\u201344","DOI":"10.1007\/3-540-36469-2_3"},{"key":"21_CR16","volume-title":"The Universal Computer: The Road from Leibniz to Turing","author":"M. Davis","year":"2000","unstructured":"Davis, M.: The Universal Computer: The Road from Leibniz to Turing. W. W. Norton & Co., Inc., New York (2000)"},{"key":"21_CR17","unstructured":"de Bruijn, N.G.: A Survey of the Project Automath. To H.B. Curry: Essays on Combinatory Logic, 579\u2013606 (1980)"},{"key":"21_CR18","unstructured":"Encyclop\u00e9die ou dictionnaire raisonn\u00e9 des sciences, des arts et des m\u00e9tiers, pp. 1751\u20131772"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Engelbart, D.: A research center for augmenting human intellect (demo) (December 1968), http:\/\/en.wikipedia.org\/wiki\/The_Mother_of_All_Demos","DOI":"10.1145\/1476589.1476645"},{"key":"21_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/1041791.1041795","volume":"38","author":"W.M. Farmer","year":"2004","unstructured":"Farmer, W.M.: MKM: A new interdisciplinary field of research. ACM SIGSAM Bulletin\u00a038, 47\u201352 (2004)","journal-title":"ACM SIGSAM Bulletin"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Farmer, W.M.: Mathematical knowledge management. In: Schwartz, D.G. (ed.) Encyclopedia of Knowledge Management. Information Science Reference, pp. 599\u2013604 (2005)","DOI":"10.4018\/978-1-59140-573-3.ch078"},{"key":"21_CR22","unstructured":"Frege, G.: Begriffsschrift: eine der arithmetische nachgebildete Formelsprache des reinen Denkens. L. Nebert, Halle a\/S (1879\/1997)"},{"issue":"1","key":"21_CR23","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme. Monatshefte f\u00fcr Mathematik und Physik\u00a038(1), 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Guidi, F., Schena, I.: A query language for a metadata framework about mathematical resources. In: Asperti, et al. (eds.) [4], pp. 105\u2013118","DOI":"10.1007\/3-540-36469-2_9"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Heeren, B., Jeuring, J., van Leeuwen, A., Gerdes, A.: Specifying strategies for exercises. In: Autexier, et al. (eds.) [6], pp. 430\u2013445","DOI":"10.1007\/978-3-540-85110-3_36"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Horozal, F.F., Brown, C.E.: Formal representation of mathematics in a dependently typed set theory. In: Kauers, et al. (eds.) [27], pp. 265\u2013279","DOI":"10.1007\/978-3-540-73086-6_22"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Towards Mechanized Mathematical Assistants","year":"2007","unstructured":"Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.): MKM\/CALCULEMUS 2007. LNCS, vol.\u00a04573. Springer, Heidelberg (2007)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Kohlhase, A., Kohlhase, M.: An exploration in the space of mathematical knowledge. In: Kohlhase (ed.) [29], pp. 17\u201332","DOI":"10.1007\/11618027_2"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematical Knowledge Management","year":"2006","unstructured":"Kohlhase, M. (ed.): MKM 2005. LNCS, vol.\u00a03863. Springer, Heidelberg (2006)"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Libbrecht, P., Desmoulins, C., Mercat, C., Laborde, C., Dietrich, M., Hendriks, M.: Cross-curriculum search for Intergeo. In: Autexier, et al. (eds.) [6], pp. 520\u2013535","DOI":"10.1007\/978-3-540-85110-3_42"},{"key":"21_CR31","unstructured":"Mathematical Knowledge Management Symposium, http:\/\/www.macs.hw.ac.uk\/~fairouz\/mkm-symposium03\/"},{"issue":"1-3","key":"21_CR32","first-page":"47","volume":"38","author":"E. Melis","year":"2003","unstructured":"Melis, E., B\u00fcdenbender, J., Goguadze, G., Libbrecht, P., Ullrich, C.: Knowledge representation and management in activemath. Ann. Math. Artif. Intell.\u00a038(1-3), 47\u201364 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"21_CR33","unstructured":"A North American Workshop on Mathematical Knowledge Management (NA-MKM 2002) (2002), http:\/\/imps.mcmaster.ca\/na-mkm-2002\/"},{"key":"21_CR34","unstructured":"Second North American Workshop on Mathematical Knowledge Management (NA-MKM 2004) (2004), http:\/\/imps.mcmaster.ca\/na-mkm-2004\/"},{"key":"21_CR35","unstructured":"Workshop on Mathematical Knowledge Management: Sustainability, Scalability and Interoperability, http:\/\/projects.cs.dal.ca\/ddrive\/seminars\/mkm.shtml"},{"key":"21_CR36","unstructured":"Nederpelt, R., Geuvers, J., de Vrijer, R.: Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics\u00a0133 (1994)"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Padovani, L.: On the roles of LaTeX and MathML in encoding and processing mathematical expressions. In: Asperti, et al. (eds.) [4], pp. 66\u201379","DOI":"10.1007\/3-540-36469-2_6"},{"key":"21_CR38","first-page":"429","volume-title":"On a \u201dbuzzword\u201d: hierarchical structure","author":"D.L. Parnas","year":"2002","unstructured":"Parnas, D.L.: On a \u201dbuzzword\u201d: hierarchical structure, pp. 429\u2013440. Springer, Heidelberg (2002)"},{"key":"21_CR39","doi-asserted-by":"publisher","first-page":"80","DOI":"10.2307\/2267329","volume":"13","author":"A.M. Turing","year":"1948","unstructured":"Turing, A.M.: Practical forms of type theory. Journal of Symbolic Logic\u00a013, 80\u201394 (1948)","journal-title":"Journal of Symbolic Logic"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Urban, J.: XML-izing Mizar: Making semantic processing and presentation of mml easy. In: Kohlhase (ed.) [29], pp. 346\u2013360","DOI":"10.1007\/11618027_23"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Verchinine, K., Lyaletski, A.V., Paskevich, A., Anisimov, A.: On correctness of mathematical texts from a logical and practical point of view. In: Autexier, et al. (eds.) [6], pp. 583\u2013598","DOI":"10.1007\/978-3-540-85110-3_47"},{"key":"21_CR42","volume-title":"Principia Mathematica","author":"A.N. Whitehead","year":"1910","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica. Cambridge University Press, Cambridge (1910)"},{"issue":"23","key":"21_CR43","first-page":"121","volume":"10","author":"F. Wiedijk","year":"2007","unstructured":"Wiedijk, F.: The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric\u00a010(23), 121\u2013133 (2007)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Youssef, A.: Roles of math search in mathematics. In: Borwein, Farmer (eds.) [7], pp. 2\u201316","DOI":"10.1007\/11812289_2"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Youssef, A.: Methods of relevance ranking and hit-content generation in math search. In: Kauers, et al. (eds.) [27], pp. 393\u2013406","DOI":"10.1007\/978-3-540-73086-6_31"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T05:41:04Z","timestamp":1558417264000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}