{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:02:48Z","timestamp":1771059768530,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_5","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"67-72","source":"Crossref","is-referenced-by-count":30,"title":["A Brief Overview of Mizar"],"prefix":"10.1007","author":[{"given":"Adam","family":"Naumowicz","sequence":"first","affiliation":[]},{"given":"Artur","family":"Korni\u0142owicz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-36469-2_10","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2003","unstructured":"Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 119\u2013132. Springer, Heidelberg (2003)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-73086-6_17","volume-title":"Towards Mechanized Mathematical Assistants","author":"E. Borak","year":"2007","unstructured":"Borak, E., Zalewska, A.: Mizar course in logic and set theory. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS, vol.\u00a04573, pp. 191\u2013204. Springer, Heidelberg (2007)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"key":"5_CR4","unstructured":"Fitch, F.B.: Symbolic Logic. An Introduction. The Ronald Press Company (1952)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar Mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 203\u2013220. Springer, Heidelberg (1996)"},{"key":"5_CR6","unstructured":"Ja\u015bkowski, S.: On the rules of supposition in formal logic. Studia Logica\u00a01 (1934)"},{"issue":"1","key":"5_CR7","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications\u00a04(1), 3\u201324 (2005)","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"5_CR8","unstructured":"Mizar home page: \n                    \n                      http:\/\/mizar.org"},{"key":"5_CR9","unstructured":"Naumowicz, A.: Teaching How to Write a Proof. In: Formed 2008: Formal Methods in Computer Science Education, pp. 91\u2013100 (2008)"},{"key":"5_CR10","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":"5_CR11","doi-asserted-by":"crossref","unstructured":"Ono, K.: On a practical way of describing formal deductions. Nagoya Mathematical Journal\u00a021 (1962)","DOI":"10.1017\/S0027763000023795"},{"key":"5_CR12","unstructured":"QED Manifesto: \n                    \n                      http:\/\/www.rbjones.com\/rbjpub\/logic\/qedres00.htm"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-48256-3_14","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Syme","year":"1999","unstructured":"Syme, D.: Three tactic theorem proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 203\u2013220. Springer, Heidelberg (1999)"},{"issue":"1","key":"5_CR14","first-page":"9","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Tarski Grothendieck set theory. Formalized Mathematics\u00a01(1), 9\u201311 (1990)","journal-title":"Formalized Mathematics"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/11618027_23","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2006","unstructured":"Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS, vol.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"5_CR16","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1023\/A:1021935419355","volume":"29","author":"M. Wenzel","year":"2002","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. Journal of Automated Reasoning\u00a029(3-4), 389\u2013411 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44755-5_26","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Wiedijk","year":"2001","unstructured":"Wiedijk, F.: Mizar Light for HOL Light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 378\u2013393. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:34:11Z","timestamp":1552120451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}