{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:35Z","timestamp":1761611075272,"version":"3.41.0"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"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":[[1999,11]]},"DOI":"10.1023\/a:1006218513245","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"197-234","source":"Crossref","is-referenced-by-count":32,"title":["On Equivalents of Well-Foundedness"],"prefix":"10.1007","volume":"23","author":[{"given":"Piotr","family":"Rudnicki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Trybulec","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"236896_CR1","unstructured":"Bancerek, G.: Directed sets, nets, ideals, filters, and maps, Formalized Mathematics, 1997, to appear."},{"issue":"2","key":"236896_CR2","first-page":"377","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Cardinal numbers, Formalized Mathematics\n1(2) (1990), 377-382.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR3","first-page":"91","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: The ordinal numbers, Formalized Mathematics\n1(1) (1990), 91-96.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR4","first-page":"281","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Sequences of ordinal numbers, Formalized Mathematics\n1(2) (1990), 281-290.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR5","first-page":"123","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: The well ordering relations, Formalized Mathematics\n1(1) (1990), 123-129.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR6","first-page":"265","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Zermelo theorem and axiom of choice, Formalized Mathematics\n1(2) (1990), 265-267.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR7","doi-asserted-by":"crossref","first-page":"65","DOI":"10.2478\/v10037-010-0009-7","volume":"2","author":"G. Bancerek","year":"1991","unstructured":"Bancerek, G.: Countable sets and Hessenberg' theorem, Formalized Mathematics\n2(1) (1991), 65-69.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"236896_CR8","first-page":"397","volume":"2","author":"G. Bancerek","year":"1991","unstructured":"Bancerek, G.: K\u00f6nig' lemma, Formalized Mathematics\n2(3) (1991), 397-402.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR9","first-page":"89","volume":"3","author":"G. Bancerek","year":"1992","unstructured":"Bancerek, G.: On powers of cardinals, Formalized Mathematics\n3(1) (1992), 89-93.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR10","first-page":"107","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G. and Hryniewiecki, K.: Segments of natural numbers and finite sequences, Formalized Mathematics\n1(1) (1990), 107-114.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"236896_CR11","first-page":"485","volume":"5","author":"G. Bancerek","year":"1996","unstructured":"Bancerek, G. and Trybulec, A.: Miscellaneous facts about functions, Formalized Mathematics\n5(4) (1996), 485-492.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"236896_CR12","first-page":"433","volume":"1","author":"J. Bia\u0142as","year":"1990","unstructured":"Bia\u0142as, J.: Group and field definitions, Formalized Mathematics\n1(3) (1990), 433-439.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"236896_CR13","first-page":"353","volume":"5","author":"J. Bia\u0142as","year":"1996","unstructured":"Bia\u0142as, J. and Nakamura, Y.: The theorem ofWeierstrass, Formalized Mathematics\n5(3) (1996), 353-359.","journal-title":"Formalized Mathematics"},{"key":"236896_CR14","doi-asserted-by":"crossref","unstructured":"Boyer, R. S.: A mechanically proof-checked Encyclopedia of Mathematics: Should we build one? Can we? in A. Bundy (ed.), 12th International Conference on Automated Deduction LNAI\/LNCS 814, Springer-Verlag, 1994, pp. 237-251.","DOI":"10.1007\/3-540-58156-1_17"},{"issue":"4","key":"236896_CR15","first-page":"669","volume":"1","author":"C. Byli\u0144ski","year":"1990","unstructured":"Byli\u0144ski, C.: A classical first order language, Formalized Mathematics\n1(4) (1990), 669-676.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR16","first-page":"55","volume":"1","author":"C. Byli\u0144nski","year":"1990","unstructured":"Byli\u0144nski, C.: Functions and their basic properties, Formalized Mathematics\n1(1) (1990), 55-65.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR17","first-page":"357","volume":"1","author":"C. Byli\u0144nski","year":"1990","unstructured":"Byli\u0144nski, C.: Partial functions, Formalized Mathematics\n1(2) (1990), 357-367.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR18","first-page":"47","volume":"1","author":"C. Byli\u0144nski","year":"1990","unstructured":"Byli\u0144nski, C.: Some basic properties of sets, Formalized Mathematics\n1(1) (1990), 47-53.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR19","first-page":"165","volume":"1","author":"A. Darmochwa\u0142","year":"1990","unstructured":"Darmochwa\u0142, A.: Finite sets, Formalized Mathematics\n1(1) (1990), 165-167.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR20","first-page":"309","volume":"2","author":"A. Darmochwa\u0142","year":"1991","unstructured":"Darmochwa\u0142, A.: Calculus of quantifiers: Deduction theorem, Formalized Mathematics\n2(2) (1991), 309-312.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"236896_CR21","first-page":"609","volume":"2","author":"A. Darmochwa\u0142","year":"1991","unstructured":"Darmochwa\u0142, A. and Nakamura, Y.: Heine-Borel' covering theorem, FormalizedMathematics\n2(4) (1991), 609-610.","journal-title":"FormalizedMathematics"},{"issue":"4","key":"236896_CR22","first-page":"505","volume":"2","author":"A. de la Cruz","year":"1991","unstructured":"de la Cruz, A.: Fix point theorem for compact spaces, Formalized Mathematics\n2(4) (1991), 505-506.","journal-title":"Formalized Mathematics"},{"key":"236896_CR23","unstructured":"Franz\u00e9n, T.: Teaching mathematics through formalism: A few caveats, in D. Gries (ed.), Proceedings of the DIMACS Symposium on Teaching Logic, DIMACS, 1996. On WWW: http:\/\/dimacs.rutgers.edu\/Workshops\/Logic\/program.html."},{"key":"236896_CR24","doi-asserted-by":"crossref","unstructured":"Gries, D. and Schneider, F. B.: A Logical Approach to Discrete Math., Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4757-3837-7"},{"key":"236896_CR25","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Inductive definitions: Automation and application, in Proceedings of the 1995 International Workshop on Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Comput. Sci. 971, Springer-Verlag, 1995, pp. 200-213.","DOI":"10.1007\/3-540-60275-5_66"},{"key":"236896_CR26","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A Mizar mode for HOL, in J. von Wright, J. Grundy, and J. Harrison (eds.), Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Turku, Finland, Lecture Notes in Comput. Sci. 1125, Springer-Verlag, 1996, pp. 203-220.","DOI":"10.1007\/BFb0105406"},{"key":"236896_CR27","unstructured":"Hayden, S. and Kennison, J. F.: Zermelo Fraenkel Set Theory, Charles E. Merrill Publishing Co., Columbus, Ohio, 1968."},{"issue":"1","key":"236896_CR28","first-page":"35","volume":"1","author":"K. Hryniewiecki","year":"1990","unstructured":"Hryniewiecki, K.: Basic properties of real numbers, Formalized Mathematics\n1(1) (1990), 35-40.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR29","first-page":"321","volume":"1","author":"K. Hryniewiecki","year":"1990","unstructured":"Hryniewiecki, K.: Recursive definitions, Formalized Mathematics\n1(2) (1990), 321-328.","journal-title":"Formalized Mathematics"},{"key":"236896_CR30","unstructured":"Ja\u015bkowski, S.: On the rules of supposition in formal logic, Studia Logica\n1 (1934)."},{"issue":"5","key":"236896_CR31","first-page":"675","volume":"2","author":"M. Korolkiewicz","year":"1991","unstructured":"Korolkiewicz, M.: The de l'Hospital theorem, Formalized Mathematics\n2(5) (1991), 675-678.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"236896_CR32","first-page":"803","volume":"1","author":"J. Kotowicz","year":"1990","unstructured":"Kotowicz, J., Raczkowski, K. and Sadowski, P.: Average value theorems for real functions of one variable, Formalized Mathematics\n1(4) (1990), 803-805.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR33","first-page":"13","volume":"2","author":"E. Kusak","year":"1991","unstructured":"Kusak, E.: Desargues theorem in projective 3-space, Formalized Mathematics\n2(1) (1991), 13-16.","journal-title":"Formalized Mathematics"},{"key":"236896_CR34","series-title":"Research Report","volume-title":"How to write a proof","author":"L. Lamport","year":"1993","unstructured":"Lamport, L.: How to write a proof, Research Report 94, DEC Systems Reserach Center, Palo Alto, CA, 1993."},{"key":"236896_CR35","volume-title":"Polish Logic in 1920-1939","author":"S. McCall","year":"1967","unstructured":"McCall, S. (ed.): Polish Logic in 1920-1939, Clarendon Press, Oxford, 1967."},{"issue":"1","key":"236896_CR36","first-page":"29","volume":"4","author":"B. Nowak","year":"1993","unstructured":"Nowak, B. and Trybulec, A.: Hahn-Banach theorem, Formalized Mathematics\n4(1) (1993), 29-34.","journal-title":"Formalized Mathematics"},{"key":"236896_CR37","doi-asserted-by":"crossref","unstructured":"Ono, K.: On a practical way of describing formal deductions, Nagoya Math. J.\n21 (1962).","DOI":"10.1017\/S0027763000023795"},{"issue":"1","key":"236896_CR38","first-page":"111","volume":"2","author":"J. Popio\u0142ek","year":"1991","unstructured":"Popio\u0142ek, J.: Real normed space, Formalized Mathematics\n2(1) (1991), 111-115.","journal-title":"Formalized Mathematics"},{"key":"236896_CR39","unstructured":"Rudnicki, P. and Trybulec, A.: How to write a proof, Technical Report 96-08, University of Alberta, Department of Computing Science, 1996. 19 pages."},{"key":"236896_CR40","unstructured":"Rudnicki, P. and Trybulec, A.: Fix-points in complete lattices, Formalized Mathematics (1997), to appear."},{"key":"236896_CR41","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, Fund. Math.\n32 (1939), 176-183.","journal-title":"Fund. Math."},{"issue":"1","key":"236896_CR42","first-page":"13","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Built-in concepts, Formalized Mathematics\n1(1) (1990), 13-15.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"236896_CR43","first-page":"495","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Function domains and Fr\u00e6nkel operator, Formalized Mathematics\n1(3) (1990), 495-500.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR44","first-page":"9","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Tarski Grothendieck set theory, Formalized Mathematics\n1(1) (1990), 9-11.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR45","first-page":"313","volume":"1","author":"W. A. Trybulec","year":"1990","unstructured":"Trybulec, W. A.: Partially ordered sets, Formalized Mathematics\n1(2) (1990), 313-319.","journal-title":"Formalized Mathematics"},{"issue":"5","key":"236896_CR46","first-page":"855","volume":"1","author":"W. A. Trybulec","year":"1990","unstructured":"Trybulec, W. A.: Subgroup and cosets of subgroups, Formalized Mathematics\n1(5) (1990), 855-864.","journal-title":"Formalized Mathematics"},{"issue":"2","key":"236896_CR47","first-page":"387","volume":"1","author":"W. A. Trybulec","year":"1990","unstructured":"Trybulec, W. A. and Bancerek, G.: Kuratowski-Zorn lemma, Formalized Mathematics\n1(2) (1990), 387-393.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR48","first-page":"17","volume":"1","author":"Z. Trybulec","year":"1990","unstructured":"Trybulec, Z. and \u015awi\u0119czkowska, H.: Boolean properties of sets, Formalized Mathematics\n1(1) (1990), 17-23.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR49","first-page":"45","volume":"4","author":"J. S. Walijewski","year":"1993","unstructured":"Walijewski, J. S.: Representation theorem for Boolean algebras, Formalized Mathematics\n4(1) (1993), 45-50.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR50","first-page":"85","volume":"3","author":"T. Watanabe","year":"1992","unstructured":"Watanabe, T.: The Brouwer fixed point theorem for intervals, Formalized Mathematics\n3(1) (1992), 85-88.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR51","first-page":"73","volume":"1","author":"E. Woronowicz","year":"1990","unstructured":"Woronowicz, E.: Relations and their basic properties, Formalized Mathematics\n1(1) (1990), 73-83.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"236896_CR52","first-page":"181","volume":"1","author":"E. Woronowicz","year":"1990","unstructured":"Woronowicz, E.: Relations defined on sets, Formalized Mathematics\n1(1) (1990), 181-186.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"236896_CR53","first-page":"423","volume":"5","author":"M. \u017bynel","year":"1996","unstructured":"\u017bynel, M.: The Steinitz theorem and the dimension of a vector space, Formalized Mathematics\n5(3) (1996), 423-428.","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:1006218513245.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006218513245\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006218513245.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:25:27Z","timestamp":1749122727000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006218513245"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,11]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,11]]}},"alternative-id":["236896"],"URL":"https:\/\/doi.org\/10.1023\/a:1006218513245","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1999,11]]}}}