{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:49:41Z","timestamp":1777423781559,"version":"3.51.4"},"reference-count":17,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80758-8","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"69-85","source":"Crossref","is-referenced-by-count":17,"title":["On the Structure of Mizar Types"],"prefix":"10.1016","volume":"85","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB1","series-title":"\u201cSymbolic Computation and Automated Reasoning\u201d","article-title":"Development of the theory of continuous lattices in mizar","author":"Bancerek","year":"2001"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB2","first-page":"29","article-title":"Lim-inf convergence and its compactness","volume":"2","author":"Bancerek","year":"2002","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB3","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1021966832558","article-title":"A compendium of continuous lattices in MIZAR","volume":"29","author":"Bancerek","year":"2002","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB4","series-title":"Fondation Ph. le Hodey","article-title":"\u201cAn introduction to PC Mizar,\u201d","author":"Bonarska","year":"1990"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB5","unstructured":"Kamareddine F., and R. Nederpelt, A refinement of de Bruijn's formal language of mathematics, to appear, 2003."},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB6","first-page":"1","article-title":"Algebraic requirements for the construction of polynomial rings","volume":"2","author":"Milewski","year":"2002","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB7","series-title":"Fondation Ph le Hodey","article-title":"\u201cAn outline to PC Mizar,\u201d","author":"Muzalewski","year":"1993"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB8","unstructured":"Nakamura Y., \u201cMizar lectures notes,\u201d 4th edition. Shinshu University, Nagano, 2001. http:\/\/markun.cs.shinshu-u.ac.jp\/kiso\/projects2\/proofchecker\/mizar\/Mizar4\/index-e.html"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB9","unstructured":"Rudnicki P., An overview of the Mizar project, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992. http:\/\/mizar.org\/project\/MizarOverview.ps.gz"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/jsco.2001.0456","article-title":"Commutative algebra in the Mizar System","volume":"32","author":"Rudnicki","year":"2001","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB11","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","article-title":"On equivalents of well-foundedness","volume":"23","author":"Rudnicki","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB12","unstructured":"Trybulec A., Informationslogische sprache Mizar, Dokumentation-Information, Heft 33, Ilmenau, 1977."},{"issue":"No. 2.","key":"10.1016\/S1571-0661(04)80758-8_NEWBIB13","article-title":"The Mizar-QC\/6000 Logic Information Language","volume":"6","author":"Trybulec","year":"1978","journal-title":"ALLC Bulletin"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB14","article-title":"The Mizar Logic Information Language","volume":"1","author":"Trybulec","year":"1980","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB15","series-title":"\u201cMKM 2003\u201d","first-page":"203","article-title":"Translating Mizar for first order theorem provers","author":"Urban","year":"2003"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB16","series-title":"\u201cMKM 2003\u201d","first-page":"188","article-title":"Comparing mathematical provers","author":"Wiedijk","year":"2003"},{"key":"10.1016\/S1571-0661(04)80758-8_NEWBIB17","unstructured":"Wiedijk F., \u201cMizar: An Impression,\u201d http:\/\/www.cs.kun.nl\/~freek\/notes"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807588?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807588?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T05:53:10Z","timestamp":1549173190000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104807588"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":17,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066104807588"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80758-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}