{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T03:09:15Z","timestamp":1768014555729,"version":"3.49.0"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021966832558","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"189-224","source":"Crossref","is-referenced-by-count":23,"title":["A Compendium of Continuous Lattices in MIZAR"],"prefix":"10.1007","volume":"29","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Rudnicki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"5109767_CR1","first-page":"563","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Tarski's classes and ranks, Formalized Mathematics\n1(3) (1990), 563\u2013567. MML: CLASSES1.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"5109767_CR2","first-page":"589","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: K\u00f6nig's theorem, Formalized Mathematics\n1(3) (1990), 589\u2013593. MML: CARD_3.","journal-title":"Formalized Mathematics"},{"issue":"5","key":"5109767_CR3","first-page":"719","volume":"2","author":"G. Bancerek","year":"1991","unstructured":"Bancerek, G.: Complete lattices, Formalized Mathematics\n2(5) (1991), 719\u2013725. MML: LATTICE3.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR4","first-page":"81","volume":"6","author":"G. Bancerek","year":"1997","unstructured":"Bancerek, G.: Bounds in posets and relational substructures, Formalized Mathematics\n6(1) (1997), 81\u201391. MML: YELLOW_0.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR5","first-page":"93","volume":"6","author":"G. Bancerek","year":"1997","unstructured":"Bancerek, G.: Directed sets, nets, ideals, filters, and maps, Formalized Mathematics\n6(1) (1997), 93\u2013107. MML: WAYBEL_0.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR6","first-page":"169","volume":"6","author":"G. Bancerek","year":"1997","unstructured":"Bancerek, G.: The \u201cway-below\u201d relation, FormalizedMathematics\n6(1) (1997), 169\u2013176. MML: WAYBEL_3.","journal-title":"FormalizedMathematics"},{"issue":"2","key":"5109767_CR7","first-page":"227","volume":"6","author":"G. Bancerek","year":"1997","unstructured":"Bancerek, G.: Duality in relation structures, Formalized Mathematics\n6(2) (1997), 227\u2013232. MML: YELLOW_7.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR8","first-page":"241","volume":"6","author":"G. Bancerek","year":"1997","unstructured":"Bancerek, G.: Prime ideals and filters, Formalized Mathematics\n6(2) (1997), 241\u2013247. MML","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR9","first-page":"35","volume":"7","author":"G. Bancerek","year":"1998","unstructured":"Bancerek, G.: Bases and refinements of topologies, Formalized Mathematics\n7(1) (1998), 35\u201343. MML: YELLOW_9.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR10","first-page":"163","volume":"7","author":"G. Bancerek","year":"1998","unstructured":"Bancerek, G.: The Lawson topology, Formalized Mathematics\n7(2) (1998), 163\u2013168. MML: WAYBEL19.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR11","first-page":"177","volume":"7","author":"G. Bancerek","year":"1998","unstructured":"Bancerek, G.: Lawson topology in continuous lattices, Formalized Mathematics\n7(2) (1998), 177\u2013184. MML: WAYBEL21.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR12","unstructured":"Bancerek, G.: Development of the theory of continuous lattices in MIZAR, in M. Kerber and M. Kohlhase (eds), Symbolic Computation and Automated Reasoning, A. K. Peters, 2001."},{"issue":"1","key":"5109767_CR13","first-page":"111","volume":"9","author":"G. Bancerek","year":"2001","unstructured":"Bancerek, G.: Continuous lattices of maps between T0 spaces, Formalized Mathematics\n9(1) (2001), 111\u2013117. MML: WAYBEL26.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"5109767_CR14","first-page":"755","volume":"9","author":"G. Bancerek","year":"2001","unstructured":"Bancerek, G.: Categorial background for duality theory, Formalized Mathematics\n9(4) (2001), 755\u2013765. MML: YELLOW21.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"5109767_CR15","first-page":"767","volume":"9","author":"G. Bancerek","year":"2001","unstructured":"Bancerek, G.: Duality based on the Galois connection. Part I, Formalized Mathematics\n9(4) (2001), 767\u2013778. MML: WAYBEL34.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR16","first-page":"29","volume":"2","author":"G. Bancerek","year":"2002","unstructured":"Bancerek, G., Endou, N. and Shidama, Y.: Lim-inf convergence and its compactness, Mechanized Mathematics and Its Applications\n2(1) (2002), 29\u201335.","journal-title":"Mechanized Mathematics and Its Applications"},{"issue":"1","key":"5109767_CR17","first-page":"47","volume":"1","author":"C. Byli\u00b4nski","year":"1990","unstructured":"Byli\u00b4nski, C.: Some basic properties of sets, Formalized Mathematics\n1(1) (1990), 47\u201353. MML: ZFMISC_1.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR18","first-page":"409","volume":"1","author":"C. Byli\u00b4nski","year":"1990","unstructured":"Byli\u00b4nski, C.: Introduction to categories and functors, Formalized Mathematics\n1(2) (1990), 409\u2013420. MML: CAT_1.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"5109767_CR19","first-page":"527","volume":"2","author":"C. Byli\u00b4nski","year":"1991","unstructured":"Byli\u00b4nski, C.: Category ens, Formalized Mathematics\n2(4) (1991), 527\u2013533. MML: ENS_1.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR20","first-page":"131","volume":"6","author":"C. Byli\u00b4nski","year":"1997","unstructured":"Byli\u00b4nski, C.: Galois connections, Formalized Mathematics\n6(1) (1997), 131\u2013143. MML: WAYBEL_1.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"5109767_CR21","first-page":"441","volume":"6","author":"C. Byli\u00b4nski","year":"1997","unstructured":"Byli\u00b4nski, C. and Rudnicki, P.: The Scott topology. Part II, Formalized Mathematics\n6(3) (1997), 441\u2013446. MML: WAYBEL14.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR22","doi-asserted-by":"crossref","unstructured":"Fleuriot, J. and Paulson, L. C.: A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia, in C. Kirchner and H. Kirchner (eds), 15th International Conf. on Automated Deduction: CADE-15, LNAI 1421, Springer, 1998, pp. 3\u201316.","DOI":"10.1007\/BFb0054241"},{"key":"5109767_CR23","doi-asserted-by":"crossref","unstructured":"Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. W. and Scott, D. S.: A Compendium of Continuous Lattices, Springer-Verlag, Berlin, 1980.","DOI":"10.1007\/978-3-642-67678-9"},{"issue":"1","key":"5109767_CR24","first-page":"117","volume":"6","author":"A. Grabowski","year":"1997","unstructured":"Grabowski, A. and Milewski, R.: Boolean posets, posets under inclusion and products of relational structures, Formalized Mathematics\n6(1) (1997), 117\u2013121. MML: YELLOW_1.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR25","first-page":"57","volume":"7","author":"J. Gryko","year":"1998","unstructured":"Gryko, J.: Injective spaces, Formalized Mathematics\n7(1) (1998), 57\u201362. MML: WAYBEL18.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR26","volume-title":"On the Rules of Supposition in Formal Logic","author":"S. Ja\u00b4skowski","year":"1934","unstructured":"Ja\u00b4skowski, S.: On the Rules of Supposition in Formal Logic, Studia Logica,Warsaw University, 1934. Reprinted in S. McCall, Polish Logic in 1920\u20131939, Clarendon Press, Oxford."},{"key":"5109767_CR27","volume-title":"Stone Spaces","author":"P. T. Johnstone","year":"1982","unstructured":"Johnstone, P. T.: Stone Spaces, Cambridge University Press, Cambridge, 1982."},{"key":"5109767_CR28","unstructured":"van Benthem Jutting, L. S.: Checking Landau's \u201cGrundlagen\u201d in the Automath system, Ph.D. thesis, The Eindhoven, 1977."},{"key":"5109767_CR29","unstructured":"Kelley, J. L.: General Topology, Van Nostrand, New York, 1955."},{"issue":"1","key":"5109767_CR30","first-page":"145","volume":"6","author":"A. Korni\u0142owicz","year":"1997","unstructured":"Korni\u0142owicz, A.: Cartesian products of relations and relational structures, Formalized Mathematics\n6(1) (1997), 145\u2013152. MML: YELLOW_3.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR31","first-page":"269","volume":"6","author":"A. Korni\u0142owicz","year":"1997","unstructured":"Korni\u0142owicz, A.: On the topological properties of meet-continuous lattices, Formalized Mathematics\n6(2) (1997), 269\u2013277. MML: WAYBEL_9.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR32","unstructured":"Landau, E. G. H.: Grundlagen der Analysis, Akademische Verlag, Leipzig, 1930."},{"key":"5109767_CR33","unstructured":"Library Committee of the Association of Mizar Users. Preliminaries to Structures, JFM, Addenda. MML: STRUCT_0."},{"key":"5109767_CR34","unstructured":"Library Committee of the Association of Mizar Users. Preliminaries to Arithmetic, JFM, Addenda. MML: ARYTM."},{"key":"5109767_CR35","unstructured":"MIZAR Manuals. http:\/\/mizar.org\/project\/bibliography.html."},{"issue":"1","key":"5109767_CR36","first-page":"103","volume":"4","author":"B. Madras","year":"1993","unstructured":"Madras, B.: Product of family of universal algebras, Formalized Mathematics\n4(1) (1993), 103\u2013108. MML: PRALG_1.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR37","first-page":"249","volume":"6","author":"R. Milewski","year":"1997","unstructured":"Milewski, R.: Algebraic lattices, Formalized Mathematics\n6(2) (1997), 249\u2013254. MML: WAYBEL_8.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR38","unstructured":"Nederpelt, R. P., Geuvers, J. H. and de Vrijer, R. C.: Selected Papers on Automath, North-Holland, Amsterdam, 1994."},{"key":"5109767_CR39","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook, Formal Aspects of Computing\n10 (1998), 171\u2013186.","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"5109767_CR40","first-page":"223","volume":"1","author":"B. Padlewska","year":"1990","unstructured":"Padlewska, B. and Darmochwa\u0142, A.: Topological spaces and continuous functions, Formalized Mathematics\n1(1) (1990), 223\u2013230. MML: PRE_TOPC.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR41","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"L. C. Paulson","year":"1996","unstructured":"Paulson, L. C. and Grabczewski, K.: Mechanizing set theory: Cardinal arithmetic and the axiom of choice, J. Automated Reasoning\n17 (1996), 291\u2013323.","journal-title":"J. Automated Reasoning"},{"key":"5109767_CR42","volume-title":"The Mathematics of Metamathematics","author":"H. Rasiowa","year":"1968","unstructured":"Rasiowa, H. and Sikorski, R.: The Mathematics of Metamathematics, PWN, Warszawa, 1968."},{"issue":"2","key":"5109767_CR43","first-page":"169","volume":"7","author":"P. Rudnicki","year":"1998","unstructured":"Rudnicki, P.: Kernel projections and quotient lattices, Formalized Mathematics\n7(2) (1998), 169\u2013175. MML: WAYBEL20.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR44","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, Ch. and Trybulec, A.: Commutative algebra in the Mizar system, J. Symbolic Comput.\n32 (2001), 143\u2013169.","journal-title":"J. Symbolic Comput."},{"issue":"3\u20134","key":"5109767_CR45","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki, P. and Trybulec, A.: On equivalents of well-foundedness, J. Automated Reasoning\n23(3\u20134) (1999), 197\u2013234.","journal-title":"J. Automated Reasoning"},{"key":"5109767_CR46","unstructured":"Rudnicki, P. and Trybulec, A.: Mathematical knowledge management in MIZAR, 1st Int.Workshop on MKM, Sept. 24\u201326, 2001. http:\/\/www.risc.uni-linz.ac.at\/institute\/conferences\/MKM2001."},{"issue":"2","key":"5109767_CR47","first-page":"233","volume":"5","author":"A. Y. Shibakov","year":"1996","unstructured":"Shibakov, A Yu. and Trybulec, A.: The Cantor set, Formalized Mathematics\n5(2) (1996), 233\u2013236. MML: CANTOR_1.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR48","first-page":"9","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Tarski Grothendieck set theory, Formalized Mathematics\n1(1) (1990), 9\u201311. MML: TARSKI.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR49","first-page":"13","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Built-in concepts, Formalized Mathematics\n1(1) (1990), 13\u201315. MML: AXIOMS.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR50","first-page":"259","volume":"5","author":"A. Trybulec","year":"1996","unstructured":"Trybulec, A.: Categories without uniqueness of cod and dom, Formalized Mathematics\n5(2) (1996), 259\u2013267. MML: ALTCAT_1.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"5109767_CR51","first-page":"595","volume":"5","author":"A. Trybulec","year":"1996","unstructured":"Trybulec, A.: Functors for alternative categories, Formalized Mathematics\n5(4) (1996), 595\u2013608. MML: FUNCTOR0.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR52","first-page":"213","volume":"6","author":"A. Trybulec","year":"1997","unstructured":"Trybulec, A.: Moore\u2013Smith convergence, Formalized Mathematics\n6(2) (1997), 213\u2013225.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR53","first-page":"311","volume":"6","author":"A. Trybulec","year":"1997","unstructured":"Trybulec A.: Scott topology, Formalized Mathematics\n6(2) (1997), 311\u2013319. MML: WAYBEL11.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"5109767_CR54","first-page":"313","volume":"1","author":"W. A. Trybulec","year":"1990","unstructured":"Trybulec, W. A.: Partially ordered sets, Formalized Mathematics\n1(2) (1990), 313\u2013319. MML: ORDERS_1.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR55","first-page":"17","volume":"1","author":"Z. Trybulec","year":"1990","unstructured":"Trybulec, Z. and \u015awi\u00b8eczkowska, H.: Boolean properties of sets, Formalized Mathematics\n1(1) (1990), 17\u201323. MML: BOOLE.","journal-title":"Formalized Mathematics"},{"key":"5109767_CR56","unstructured":"Wiedijk, F.: Mizar: An impression. http:\/\/www.cs.kun.nl\/~freek\/notes."},{"key":"5109767_CR57","unstructured":"Wiedijk, F.: Estimating the cost of a standard library for a mathematical proof checker. http: \/\/www.cs.kun.nl\/~freek\/notes."},{"key":"5109767_CR58","unstructured":"Wiedijk, F.: The de Bruijn factor. http:\/\/www.cs.kun.nl\/~freek\/notes."},{"issue":"1","key":"5109767_CR59","first-page":"85","volume":"1","author":"E. Woronowicz","year":"1990","unstructured":"Woronowicz, E. and Zalewska, A.: Properties of binary relations, Formalized Mathematics\n1(1) (1990), 85\u201389. MML: RELAT_2.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"5109767_CR60","first-page":"215","volume":"1","author":"S. \u017bukowski","year":"1990","unstructured":"\u017bukowski, S.: Introduction to lattice theory, Formalized Mathematics\n1(1) (1990), 215\u2013222. MML: LATTICES.","journal-title":"Formalized Mathematics"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021966832558.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021966832558\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021966832558.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:28:34Z","timestamp":1749122914000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021966832558"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":60,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109767"],"URL":"https:\/\/doi.org\/10.1023\/a:1021966832558","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}