{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T00:10:59Z","timestamp":1770682259823,"version":"3.49.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T00:00:00Z","timestamp":1442275200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,10]]},"DOI":"10.1007\/s10817-015-9345-1","type":"journal-article","created":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T04:35:21Z","timestamp":1442291721000},"page":"191-198","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":105,"title":["Four Decades of Mizar"],"prefix":"10.1007","volume":"55","author":[{"given":"Adam","family":"Grabowski","sequence":"first","affiliation":[]},{"given":"Artur","family":"Korni\u0142owicz","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,15]]},"reference":[{"key":"9345_CR1","doi-asserted-by":"crossref","unstructured":"Alama, J., Kohlhase, M., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics, MKM\u201911, Lecture Notes in Computer Science, vol. 6824, pp. 149\u2013163. Springer, Berlin (2011). doi: 10.1007\/978-3-642-22673-1_11","DOI":"10.1007\/978-3-642-22673-1_11"},{"key":"9345_CR2","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Rudnicki, P.: A Compendium of Continuous Lattices in Mizar: formalizing recent mathematics. J. Autom. Reason. 29(3\u20134), 189\u2013224 (2002)","DOI":"10.1023\/A:1021966832558"},{"key":"9345_CR3","doi-asserted-by":"crossref","unstructured":"Byli\u0144ski, C., Alama, J.: New developments in parsing Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Lecture Notes in Artificial Intelligence, vol. 7362, pp. 427\u2013431. Springer, Berlin (2012). doi: 10.1007\/978-3-642-31374-5_30","DOI":"10.1007\/978-3-642-31374-5_30"},{"key":"9345_CR4","doi-asserted-by":"crossref","unstructured":"Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2\u20135, 2007, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4941, pp. 69\u201384. Springer, New York (2007). doi: 10.1007\/978-3-540-68103-8_5","DOI":"10.1007\/978-3-540-68103-8_5"},{"key":"9345_CR5","doi-asserted-by":"crossref","unstructured":"Grabowski, A.: Automated discovery of properties of rough sets. Fundam. Inform. 128(1\u20132), 65\u201379 (2013). doi: 10.3233\/FI-2013-933","DOI":"10.3233\/FI-2013-933"},{"issue":"2","key":"9345_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. Spec. Issue User Tutor. I 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason. Spec. Issue User Tutor. I"},{"key":"9345_CR7","unstructured":"Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Ganzha, M., Maciaszek, L., Paprzycki, M. (eds.) Proceedings of Federated Conference on Computer Science and Information Systems, FedCSIS 2012, pp. 63\u201368. Wroc\u0142aw, Poland (2012)"},{"key":"9345_CR8","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Kohlhase, M. (ed.) Proceedings of the 4th International Conference on Mathematical Knowledge Management, MKM\u201905, Lecture Notes in Computer Science, vol. 3863, pp. 49\u201364. Springer, Berlin (2006). doi: 10.1007\/11618027_4","DOI":"10.1007\/11618027_4"},{"key":"9345_CR9","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus \u201907 \/ MKM \u201907, Lecture Notes in Computer Science, vol. 4573, pp. 235\u2013249. Springer, Berlin (2007). doi: 10.1007\/978-3-540-73086-6_20","DOI":"10.1007\/978-3-540-73086-6_20"},{"key":"9345_CR10","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A Mizar mode for HOL. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics. TPHOLs\u201996, Lecture Notes in Computer Science, vol. 1125, pp. 203\u2013220. Springer, London, UK (1996)","DOI":"10.1007\/BFb0105406"},{"key":"9345_CR11","doi-asserted-by":"crossref","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). doi: 10.1007\/s10817-012-9271-4","DOI":"10.1007\/s10817-012-9271-4"},{"key":"9345_CR12","unstructured":"Ja\u015bkowski, S.: On the Rules of Suppositions in Formal Logic. Studia Logica. Nak\u0142adem Seminarjum Filozoficznego Wydzia\u0142u Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego (1934)"},{"key":"9345_CR13","unstructured":"Korni\u0142owicz, A.: Jordan Curve Theorem. Formaliz. Math. 13(4), 481\u2013491 (2005). http:\/\/fm.mizar.org\/2005-13\/pdf13-4\/jordan.pdf"},{"key":"9345_CR14","doi-asserted-by":"crossref","unstructured":"Korni\u0142owicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203\u2013210 (2013). doi: 10.1007\/s10817-012-9261-6","DOI":"10.1007\/s10817-012-9261-6"},{"key":"9345_CR15","doi-asserted-by":"crossref","unstructured":"Korni\u0142owicz, A.: Flexary connectives in Mizar. Computer Languages, Systems & Structures (2015). doi: 10.1016\/j.cl.2015.07.002","DOI":"10.1016\/j.cl.2015.07.002"},{"key":"9345_CR16","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: The first 30\u00a0years. Mech. Math. Appl. Special Issue on 30 Years of Mizar 4(1), 3\u201324 (2005)"},{"key":"9345_CR17","doi-asserted-by":"crossref","unstructured":"Naumowicz, A.: Interfacing external CA systems for Gr\u00f6bner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1\u201311 (2010). doi: 10.1080\/00207160701864459","DOI":"10.1080\/00207160701864459"},{"key":"9345_CR18","doi-asserted-by":"crossref","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201909, Lecture Notes in Computer Science, vol. 5674, pp. 67\u201372. Springer, Berlin (2009). doi: 10.1007\/978-3-642-03359-9_5","DOI":"10.1007\/978-3-642-03359-9_5"},{"key":"9345_CR19","doi-asserted-by":"crossref","unstructured":"Pa\u0328k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217\u2013228 (2013). doi: 10.1007\/s10817-012-9267-0","DOI":"10.1007\/s10817-012-9267-0"},{"key":"9345_CR20","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki P., Schwarzweller C., Trybulec A.: Commutative algebra in the Mizar system. J. Symb. Comput. 32, 143\u2013169 (2001)","journal-title":"J. Symb. Comput."},{"key":"9345_CR21","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki P., Trybulec A.: On equivalents of well-foundednessAn experiment in Mizar. J. Autom. Reason. 23, 197\u2013234 (1999)","journal-title":"J. Autom. Reason."},{"key":"9345_CR22","unstructured":"Rudnicki, P., Trybulec, A.: Mathematical knowledge management in Mizar. In: Buchberger, B. Caprotti, O. (eds.) Procedings of the First International Workshop on Mathematical Knowledge Management, Linz, Austria (2001)"},{"key":"9345_CR23","doi-asserted-by":"crossref","unstructured":"Rudnicki, P., Trybulec, A.: On the integrity of a repository of formal mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) Proceedings of MKM 2003, Lecture Notes in Computer Science, vol. 2594, pp. 162\u2013174. Springer, Berlin (2003). doi: 10.1007\/3-540-36469-2_13","DOI":"10.1007\/3-540-36469-2_13"},{"key":"9345_CR24","unstructured":"Syme, D.: DECLARE: A prototype declarative proof system for higher order logic. Technicl Report. University of Cambridge, Cambridge (1997)"},{"key":"9345_CR25","doi-asserted-by":"crossref","first-page":"176","DOI":"10.4064\/fm-32-1-176-783","volume":"32","author":"A. Tarski","year":"1939","unstructured":"Tarski A.: On well-ordered subsets of any set. Fundam. Math. 32, 176\u2013183 (1939)","journal-title":"Fundam. Math."},{"key":"9345_CR26","doi-asserted-by":"crossref","unstructured":"Trybulec, A.: Informationslogische sprache Mizar, Dokumentation\u2013Information, Heft 33, pp. 46\u201353. Ilmenau (1977)","DOI":"10.1111\/j.1745-7939.1977.tb00845.x"},{"issue":"2","key":"9345_CR27","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Trybulec A.: The Mizar-QC\/6000 logic information language. ALLC Bull. 6(2), 136\u2013140 (1978)","journal-title":"ALLC Bull."},{"key":"9345_CR28","unstructured":"Trybulec, A.: The Mizar logic information language. Stud. Log. Gramm. Rhetor. 1, 127\u2013136 (1980)"},{"key":"9345_CR29","unstructured":"Trybulec, A.: Tarski Grothendieck set theory. Form. Math. 1(1), 9\u201311 (1990). http:\/\/fm.mizar.org\/1990-1\/pdf1-1\/tarski.pdf"},{"key":"9345_CR30","unstructured":"Trybulec, A.: Some features of the Mizar language. In: Proceedings of ESPRIT Workshop. Torino (1993)"},{"key":"9345_CR31","doi-asserted-by":"crossref","unstructured":"Trybulec, A.: Mizar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, Lecture Notes in Computer Science, vol. 3600, pp. 20\u201323. Springer, Berlin (2006). doi: 10.1007\/11542384_4","DOI":"10.1007\/11542384_4"},{"key":"9345_CR32","doi-asserted-by":"crossref","unstructured":"Trybulec, A., Blair, H.A.: Computer aided reasoning. In: Proceedings of the Conference Logic of Programs, Lecture Notes in Computer Science vol. 193, pp. 406\u2013412. Springer, New York (1985)","DOI":"10.1007\/3-540-15648-8_30"},{"key":"9345_CR33","doi-asserted-by":"crossref","unstructured":"Trybulec, A., Korni\u0142owicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119\u2013121 (2013). doi: 10.1007\/s10817-012-9268-z","DOI":"10.1007\/s10817-012-9268-z"},{"key":"9345_CR34","unstructured":"Trybulec, A., Rudnicki, P.: A Collection of ed Mizar Abstracts. University of Alberta, Canada (1989)"},{"key":"9345_CR35","unstructured":"Trybulec, A., Rudnicki, P.: Using Mizar in computer aided instruction of mathematics. In: Norvegian-French Conference of CAI in Mathematics. Oslo (1993)"},{"key":"9345_CR36","doi-asserted-by":"crossref","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013). doi: 10.1007\/s10817-012-9269-y","DOI":"10.1007\/s10817-012-9269-y"},{"key":"9345_CR37","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3\u20134), 389\u2013411 (2003). doi: 10.1023\/A:1021935419355","DOI":"10.1023\/A:1021935419355"},{"key":"9345_CR38","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Mizar Light for HOL Light. In: Boulton, R.J., Jackson, P.B. (eds.) Proceedings of 14th International Conference TPHOLs, Lecture Notes in Computer Science, vol. 2152, pp. 378\u2013393. Springer, New York (2001)","DOI":"10.1007\/3-540-44755-5_26"},{"key":"9345_CR39","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES, Lecture Notes in Computer Science, vol. 3085, pp. 378\u2013393. Springer, New York (2004). doi: 10.1007\/978-3-540-24849-1_24","DOI":"10.1007\/978-3-540-24849-1_24"},{"key":"9345_CR40","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Log. Methods Comput. Sci. 8(1:30), 1\u201326 (2012)","DOI":"10.2168\/LMCS-8(1:30)2012"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9345-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9345-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9345-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T09:19:00Z","timestamp":1599556740000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9345-1"}},"subtitle":["Foreword"],"short-title":[],"issued":{"date-parts":[[2015,9,15]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,10]]}},"alternative-id":["9345"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9345-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,15]]}}}