{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:45:16Z","timestamp":1725936316023},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319724522"},{"type":"electronic","value":"9783319724539"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-72453-9_12","type":"book-chapter","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T09:35:54Z","timestamp":1513762554000},"page":"163-178","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Isabelle Formalization of Set Theoretic Structures and Set Comprehensions"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karol","family":"P\u0105k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,21]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.tcs.2015.07.013","volume":"603","author":"A Asperti","year":"2015","unstructured":"Asperti, A., Ricciotti, W.: A formalization of multi-tape turing machines. Theor. Comput. Sci. 603, 23\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-42547-4_8","volume-title":"Intelligent Computer Mathematics","author":"CE Brown","year":"2016","unstructured":"Brown, C.E., Urban, J.: Extracting higher-order goals from the Mizar mathematical library. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 99\u2013114. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-42547-4_8"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_14"},{"issue":"4","key":"12_CR5","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271\u2013286 (2002)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"12_CR6","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason."},{"issue":"3","key":"12_CR7","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015)","journal-title":"J. Autom. Reason."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Korni\u0142owicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the Federated Conference on Computer Science and Information Systems (FedCSIS 2016), pp. 363\u2013371 (2016)","DOI":"10.15439\/2016F520"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 160\u2013174. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74464-1_11"},{"key":"12_CR10","first-page":"135","volume-title":"Computational Logic, Handbook of the History of Logic","author":"J Harrison","year":"2014","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 135\u2013214. Elsevier, Amsterdam (2014)"},{"issue":"2","key":"12_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-012-9271-4","volume":"50","author":"M Iancu","year":"2013","unstructured":"Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191\u2013202 (2013)","journal-title":"J. Autom. Reason."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-62075-6_14","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2017","unstructured":"Kaliszyk, C., P\u0105k, K.: Presentation and manipulation of Mizar properties in an Isabelle object logic. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 193\u2013207. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-62075-6_14"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., P\u0105k, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th Conference on Certified Programs and Proofs (CPP 2016), pp. 58\u201365. ACM (2016)","DOI":"10.1145\/2854065.2854070"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., P\u0105k, K.: Progress in the independent certification of Mizar mathematical library in Isabelle. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the Federated Conference on Computer Science and Information Systems (FedCSIS 2017), pp. 227\u2013236 (2017)","DOI":"10.15439\/2017F289"},{"issue":"3","key":"12_CR15","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reason."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-02444-3_13","volume-title":"Types for Proofs and Programs","author":"C Kaliszyk","year":"2009","unstructured":"Kaliszyk, C., Wiedijk, F.: Merging procedural and declarative proof. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 203\u2013219. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02444-3_13"},{"issue":"1","key":"12_CR17","first-page":"43","volume":"4","author":"A Korni\u0142owicz","year":"2005","unstructured":"Korni\u0142owicz, A., Schwarzweller, C.: Computers and algorithms in Mizar. Mech. Math. Appl. 4(1), 43\u201350 (2005)","journal-title":"Mech. Math. Appl."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-22102-1_17"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-540-73086-6_26","volume-title":"Towards Mechanized Mathematical Assistants","author":"G Lee","year":"2007","unstructured":"Lee, G., Rudnicki, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM -2007. LNCS (LNAI), vol. 4573, pp. 327\u2013341. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73086-6_26"},{"key":"12_CR20","volume-title":"Metamath: A Computer Language for Pure Mathematics","author":"ND Megill","year":"2007","unstructured":"Megill, N.D.: Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville (2007)"},{"issue":"2","key":"12_CR21","first-page":"151","volume":"3","author":"Y Nakamura","year":"1992","unstructured":"Nakamura, Y., Trybulec, A.: A mathematical model of CPU. Formaliz. Math. 3(2), 151\u2013160 (1992)","journal-title":"Formaliz. Math."},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-08434-3_27","volume-title":"Intelligent Computer Mathematics","author":"K P\u0105k","year":"2014","unstructured":"P\u0105k, K.: Automated improving of proof legibility in the Mizar system. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 373\u2013387. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08434-3_27"},{"issue":"4","key":"12_CR23","doi-asserted-by":"crossref","first-page":"763","DOI":"10.1017\/S0960129511000107","volume":"21","author":"C Sacerdoti-Coen","year":"2011","unstructured":"Sacerdoti-Coen, C., Tassi, E.: Formalising overlap algebras in Matita. Math. Struct. Comput. Sci. 21(4), 763\u2013793 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-540-74591-4_28","volume-title":"Theorem Proving in Higher Order Logics","author":"F Wiedijk","year":"2007","unstructured":"Wiedijk, F.: Mizar\u2019s soft type system. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 383\u2013399. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74591-4_28"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_13"}],"container-title":["Lecture Notes in Computer Science","Mathematical Aspects of Computer and Information Sciences"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72453-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T09:41:30Z","timestamp":1513762890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72453-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319724522","9783319724539"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72453-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}