{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:35Z","timestamp":1725493475461},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540005681"},{"type":"electronic","value":"9783540364696"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36469-2_3","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T03:02:41Z","timestamp":1193454161000},"page":"30-44","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls"],"prefix":"10.1007","author":[{"given":"Claudio Sacerdoti","family":"Coen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,30]]},"reference":[{"key":"3_CR1","unstructured":"M. Agrawal, N. Kayal, N. Saxena, \u201cPRIMES in P\u201d, unpublished, August 2002, \nhttp:\/\/www.cse.iitk.ac.in\/users\/manindra\/primality.ps\n\n."},{"key":"3_CR2","unstructured":"A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena, \u201cMathematical Knowledge Management in HELM\u201d, in On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM2001), RISC-Linz, Austria, September 2001."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"A. Asperti, L. Padovani, C. Sacerdoti Coen, Schena, I., \u201cHELM and the semantic Math-Web\u201d. Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2001), 3\u20136 September 2001, Edinburgh, Scotland.","DOI":"10.1007\/3-540-44755-5_6"},{"key":"3_CR4","unstructured":"A. Asperti, B. Wegner, \u201cMoWGLI-A New Approach for the Content Description in Digital Documents\u201d, in Proceedings of the Ninth International Conference on Electronic Resources and the Social Role of Libraries in the Future, Section 4, Volume 1."},{"key":"3_CR5","unstructured":"O. Caprotti, H. Geuvers, and M. Oostdijk, \u201cCertified and Portable Mathematical Documents from Formal Contexts\u201d, in On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM2001), RISC-Linz, Austria, September 2001."},{"key":"3_CR6","unstructured":"Y. Coscoy. \u201cExplication textuelle de preuves pour le Calcul des Constructions Inductives\u201d, Phd. Thesis, Universit\u00e9 de Nice-Sophia Antipolis, 2000."},{"key":"3_CR7","unstructured":"A. Franke, M. Kohlhase, \u201cMBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems\u201d, to appear in Journal of Symbolic Computation."},{"key":"3_CR8","unstructured":"J. Harrison, \u201cReal Numbers in Real Applications\u201d, invited talk at Formalising Continuous Mathematics 2002 (FCM2002), 19th August 2002, Radisson Hotel, Hampton, VA, USA"},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1006\/jsco.2000.0468","volume":"23","author":"M. Kohlhase","year":"2001","unstructured":"M. Kohlhase, A. Franke, \u201cMBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems\u201d, Journal of Symbolic Computation 23:4 (2001), pp. 365\u2013402.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR10","unstructured":"Learning Technology Standards Committee of IEEE, \u201cDraft Standard for Learning Object Metadata\u201d, July 15th 2002."},{"key":"3_CR11","unstructured":"C. Mu\u00f1oz, \u201cUn calcul de substitutions pour la repr\u00e9sentation de preuves partielles en th\u00e9orie de types\u201d, PhD. Thesis, University Paris 7, 1997."},{"key":"3_CR12","unstructured":"The OpenMath Esprit Consortium, \u201cThe OpenMath Standard\u201d, O. Caprotti, D. P. Carlisle, A. M. Cohen editors."}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36469-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,10]],"date-time":"2020-01-10T06:19:17Z","timestamp":1578637157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36469-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540005681","9783540364696"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-36469-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"30 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}