{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:46:03Z","timestamp":1777427163919,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540230298","type":"print"},{"value":"9783540278184","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-27818-4_9","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T14:26:47Z","timestamp":1267108007000},"page":"116-129","source":"Crossref","is-referenced-by-count":4,"title":["Managing Heterogeneous Theories within a Mathematical Knowledge Repository"],"prefix":"10.1007","author":[{"given":"Adam","family":"Grabowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Moschner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Bancerek, G.: On the structure of Mizar types. In: Geuvers, H., Kamareddine, F. (eds.) Proc. of MLC 2003. ENTCS, vol.\u00a085(7) (2003)","DOI":"10.1016\/S1571-0661(04)80758-8"},{"key":"9_CR2","unstructured":"Bancerek, G.: Development of the theory of continuous lattices in Mizar. In: Kerber, M., Kohlhase, M. (eds.) Proceedings of the Symposium on Calculemus 2000, pp. 65\u201380 (2001)"},{"key":"9_CR3","unstructured":"Buchberger, B.: Mathematical Knowledge Management in Theorema. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)"},{"key":"9_CR4","unstructured":"Constable, R.L.: Steps toward a World Wide Digital Library of Formal Mathematics. In: MKM Symposium, Edinburgh, UK (2003)"},{"key":"9_CR5","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen, \n                  \n                    http:\/\/www.cs.kun.nl\/~freek\/notes\/"},{"key":"9_CR6","unstructured":"Davenport, J.: Mathematical knowledge representation. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction - CADE-11","author":"W. Farmer","year":"1992","unstructured":"Farmer, W., Guttman, J., Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 567\u2013581. Springer, Heidelberg (1992)"},{"key":"9_CR8","unstructured":"Giuntini, R.: Quantum Logic and Hidden Variables, Bibliographisches Institute, Mannheim (1991)"},{"issue":"4","key":"9_CR9","first-page":"681","volume":"9","author":"A. Grabowski","year":"2001","unstructured":"Grabowski, A.: Robbins algebras vs. Boolean algebras. Formalized Mathematics\u00a09(4), 681\u2013690 (2001)","journal-title":"Formalized Mathematics"},{"key":"9_CR10","unstructured":"Grabowski, A., Moschner, M.: Formalization of ortholattices via orthoposets. Formalized Mathematics (to appear, 2004)"},{"key":"9_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-7633-9","volume-title":"General Lattice Theory","author":"G. Gr\u00e4tzer","year":"1978","unstructured":"Gr\u00e4tzer, G.: General Lattice Theory. Academic Press, New York (1978)"},{"key":"9_CR12","unstructured":"Kozarkiewicz, V., Grabowski, A.: Axiomatization of lattices in terms of the Sheffer stroke. Formalized Mathematics (to appear, 2004)"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019, 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR14","unstructured":"The Mizar Home Page, \n                  \n                    http:\/\/mizar.org"},{"issue":"2","key":"9_CR15","first-page":"201","volume":"11","author":"M. Moschner","year":"2003","unstructured":"Moschner, M.: Basic notions and properties of orthoposets. Formalized Mathematics\u00a011(2), 201\u2013210 (2003)","journal-title":"Formalized Mathematics"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"9_CR17","unstructured":"Prevosto, V., Jaume, M.: Making proofs in a hierarchy of mathematical structures. In: Hardin, T., Rioboo, R. (eds.) Proceedings of Calculemus 2003, Rome, Italy (2003)"},{"key":"9_CR18","unstructured":"Rudnicki, P., Trybulec, A.: Mathematical Knowledge Management in Mizar. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-36469-2_13","volume-title":"Mathematical Knowledge Management","author":"P. Rudnicki","year":"2003","unstructured":"Rudnicki, P., Trybulec, A.: On the integrity of a repository of formalized mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 162\u2013174. Springer, Heidelberg (2003)"},{"key":"9_CR20","unstructured":"Urban, J.: MPTP 0.1. In: Dahn, I., Vigneron, L. (eds.) Proc. of FTP 2003. ENTCS, vol.\u00a086(1) (2003)"},{"key":"9_CR21","unstructured":"Wenzel, M.: Lattices and orders in Isabelle\/HOL, \n                  \n                    http:\/\/isabelle.in.tum.de\/library\/HOL\/Lattice"},{"key":"9_CR22","unstructured":"Wiedijk, F.: Formal proof sketches, \n                  \n                    http:\/\/www.cs.kun.nl\/~freek\/notes\/"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27818-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T09:08:26Z","timestamp":1552381706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27818-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230298","9783540278184"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27818-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}