{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:19:20Z","timestamp":1777425560771,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141270","type":"print"},{"value":"9783642141287","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_26","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"300-314","source":"Crossref","is-referenced-by-count":8,"title":["On Duplication in Mathematical Repositories"],"prefix":"10.1007","author":[{"given":"Adam","family":"Grabowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Schwarzweller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"The Coq Proof Assistant, \n                    \n                      http:\/\/coq.inria.fr"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-36469-2_2","volume-title":"Mathematical Knowledge Management","author":"J.H. Davenport","year":"2003","unstructured":"Davenport, J.H.: MKM from Book to Computer: A Case Study. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 17\u201329. Springer, Heidelberg (2003)"},{"key":"26_CR3","unstructured":"de Bruijn, N.G.: The Mathematical Vernacular, a language for mathematics with typed sets. In: Dybjer, P., et al. (eds.) Proceedings of the Workshop on Programming Languages, Marstrand, Sweden (1987)"},{"key":"26_CR4","volume-title":"Modern Computer Algebra","author":"J. Gathen von zur","year":"1999","unstructured":"von zur Gathen, J., Gerhard, J.: Modern Computer Algebra. Cambridge University Press, Cambridge (1999)"},{"key":"26_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11618027_4","volume-title":"Mathematical Knowledge Management","author":"A. Grabowski","year":"2006","unstructured":"Grabowski, A., Schwarzweller, C.: Translating Mathematical Vernacular into Knowledge Repositories. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 49\u201364. Springer, Heidelberg (2006)"},{"key":"26_CR6","unstructured":"Harrison, J.: The HOL Light Theorem Prover, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light"},{"issue":"1-2","key":"26_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S1567-8326(02)00065-6","volume":"50","author":"J. Hurd","year":"2003","unstructured":"Hurd, J.: Verification of the Miller-Rabin Probabilistic Primality Test. Journal of Logic and Algebraic Programming\u00a050(1-2), 3\u201321 (2003)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/3-540-51081-8_138","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1989","unstructured":"Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (RRL). In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 559\u2013563. Springer, Heidelberg (1989)"},{"issue":"3","key":"26_CR9","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/B:JLLI.0000028393.47593.b8","volume":"13","author":"F. Kamareddine","year":"2004","unstructured":"Kamareddine, F., Nederpelt, R.: A Refinement of de Bruijn\u2019s Formal Language of Mathematics. Journal of Logic, Language and Information\u00a013(3), 287\u2013340 (2004)","journal-title":"Journal of Logic, Language and Information"},{"key":"26_CR10","volume-title":"Seminumerical Algorithms","author":"D. Knuth","year":"1997","unstructured":"Knuth, D.: The Art of Computer Programming. In: Seminumerical Algorithms, 3rd edn., vol.\u00a02, Addison-Wesley, Reading (1997)","edition":"3"},{"issue":"4","key":"26_CR11","first-page":"573","volume":"6","author":"A. Kondracki","year":"1997","unstructured":"Kondracki, A.: The Chinese Remainder Theorem. Formalized Mathematics\u00a06(4), 573\u2013577 (1997)","journal-title":"Formalized Mathematics"},{"issue":"31","key":"26_CR12","first-page":"67","volume":"18","author":"A. Korni\u0142owicz","year":"2009","unstructured":"Korni\u0142owicz, A.: How to Define Terms in Mizar Effectively. Studies in Logic, Grammar and Rhetoric\u00a018(31), 67\u201377 (2009)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"26_CR13","unstructured":"L\u00fcneburg, H.: Vorlesungen \u00fcber Lineare Algebra, BI Wissenschaftsverlag (1993) (in German)"},{"key":"26_CR14","unstructured":"M\u00e9nissier-Morain, V.: A Proof of the Chinese Remainder Lemma, \n                    \n                      http:\/\/logical.saclay.inria.fr\/coq\/distrib\/current\/contribs\/ZChinese.html"},{"key":"26_CR15","unstructured":"The Mizar Home Page, \n                    \n                      http:\/\/mizar.org"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-27818-4_21","volume-title":"Mathematical Knowledge Management","author":"A. Naumowicz","year":"2004","unstructured":"Naumowicz, A., Byli\u0144ski, C.: Improving Mizar Texts with Properties and Requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 290\u2013301. Springer, Heidelberg (2004)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-27818-4_23","volume-title":"Mathematical Knowledge Management","author":"M. Pollet","year":"2004","unstructured":"Pollet, M., Sorge, V., Kerber, M.: Intuitive and Formal Representations: The Case of Matrices. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 317\u2013331. Springer, Heidelberg (2004)"},{"key":"26_CR18","unstructured":"Rudnicki, P., Trybulec, A.: Mathematical Knowledge Management in Mizar. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of the 1st International Conference on Mathematical Knowledge Management, Linz, Austria (2001)"},{"issue":"3","key":"26_CR19","doi-asserted-by":"publisher","first-page":"247","DOI":"10.2478\/v10037-008-0029-8","volume":"16","author":"C. Schwarzweller","year":"2008","unstructured":"Schwarzweller, C.: Modular Integer Arithmetic. Formalized Mathematics\u00a016(3), 247\u2013252 (2008)","journal-title":"Formalized Mathematics"},{"issue":"31","key":"26_CR20","first-page":"103","volume":"18","author":"C. Schwarzweller","year":"2009","unstructured":"Schwarzweller, C.: The Chinese Remainder Theorem, its Proofs and its Generalizations in Mathematical Repositories. Studies in Logic, Grammar and Rhetoric\u00a018(31), 103\u2013119 (2009)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"issue":"1","key":"26_CR21","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM \u2014 Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. International Journal on Artificial Intelligence Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"26_CR22","unstructured":"Wiedijk, F.: On the Usefulness of Formal Methods. In: Nieuwsbrief van de NVTI, pp. 14\u201323 (2006)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-55602-8_182","volume-title":"Automated Deduction - CADE-11","author":"H. Zhang","year":"1992","unstructured":"Zhang, H., Hua, X.: Proving the Chinese Remainder Theorem by the Cover Set Induction. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 431\u2013455. Springer, Heidelberg (1992)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:22:47Z","timestamp":1558293767000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}