{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:10:05Z","timestamp":1747548605552,"version":"3.40.5"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"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":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1023\/a:1022924032739","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T22:16:51Z","timestamp":1049753811000},"page":"193-209","source":"Crossref","is-referenced-by-count":1,"title":["Designing Mathematical Libraries Based on Requirements for Theorems"],"prefix":"10.1007","volume":"38","author":[{"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5118026_CR1","first-page":"565","volume":"9","author":"J. Backer","year":"2000","unstructured":"J. Backer, P. Rudnicki and C. Schwarzweller, Ring ideals, Formalized Mathematics 9 (2000) 565\u2013583; available by anonymous ftp from http:\/\/mizar.uwb.edu.pl\/JFM\/Vol12\/ideal_1.html.","journal-title":"Formalized Mathematics"},{"key":"5118026_CR2","volume-title":"Gr\u00f6bner Bases \u2013 A Computational Approach to Commutative Algebra","author":"T. Becker","year":"1993","unstructured":"T. Becker and V. Weispfenning, Gr\u00f6bner Bases \u2013 A Computational Approach to Commutative Algebra (Springer, Berlin, 1993)."},{"key":"5118026_CR3","doi-asserted-by":"crossref","unstructured":"B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta and D. Vasaru, A survey on the Theorema Project, in: Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation), ed. W. K\u00fcchlin (ACM Press, 1997) pp. 384\u2013391.","DOI":"10.1145\/258726.258853"},{"key":"5118026_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction \u2013 CADE-11","author":"W.M. Farmer","year":"1992","unstructured":"W.M. Farmer, J.D. Guttman and F.J. Thayer, Little theories, in: Automated Deduction \u2013 CADE-11, ed. D. Kapur, Lecture Notes in Computer Science, Vol. 607 (Springer, Berlin, 1992) pp. 567\u2013581."},{"key":"5118026_CR5","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W.M. Farmer","year":"1993","unstructured":"W.M. Farmer, J.D. Guttman and F.J. Thayer, IMPS: An Interactive Mathematical Proof System, Journal of Automated Reasoning 11 (1993) 213\u2013248.","journal-title":"Journal of Automated Reasoning"},{"key":"5118026_CR6","first-page":"335","volume":"1","author":"E. Kusak","year":"1990","unstructured":"E. Kusak, W. Leonczuk and M. Muzalewski, Abelian groups, fields and vector spaces, Formalized Mathematics 1 (1990) 335\u2013342; available by anonymous ftp from http:\/\/mizar.uwb.edu.pl\/JFM\/Vol1\/vectsp_1.html.","journal-title":"Formalized Mathematics"},{"key":"5118026_CR7","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"W. McCune, Solution of the Robbins Problem, Journal of Automated Reasoning 19 (1997) 263\u2013276.","journal-title":"Journal of Automated Reasoning"},{"key":"5118026_CR8","unstructured":"D. Musser, The Tecton Concept Description Language (1998); available by anonymous ftp from http:\/\/www.cs.rpi.edu\/~musser\/gp\/tecton."},{"key":"5118026_CR9","volume-title":"STL Tutorial and Reference Guide","author":"D. Musser","year":"2001","unstructured":"D. Musser, G. Derge and A. Saini, STL Tutorial and Reference Guide, 2nd edn., C++ Programming with the Standard Template Library (Addison-Wesley, Reading, MA, 2001).","edition":"2nd edn."},{"key":"5118026_CR10","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"P. Rudnicki and A. Trybulec, On equivalents of well-foundedness. An experiment in Mizar, Journal of Automated Reasoning 23 (1999) 197\u2013234.","journal-title":"Journal of Automated Reasoning"},{"key":"5118026_CR11","unstructured":"P. Rudnicki and A. Trybulec, Multivariate polynomials with arbitrary number of variables, Formalized Mathematics (1999), to appear; available by anonymous ftp from http:\/\/mizar.uwb.edu.pl\/JFM\/Vol11\/polynom1.html."},{"key":"5118026_CR12","unstructured":"P. Rudnicki and A. Trybulec, Mathematical knowledge management in Mizar, in: Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM2001), Linz, Austria (2001); available by anonymous ftp from http:\/\/www.risc.uni-linz.ac.at\/institute\/conferences\/MKM2001\/Proceedings\/."},{"key":"5118026_CR13","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"P. Rudnicki, C. Schwarzweller and A. Trybulec, Commutative algebra in the Mizar system, Journal of Symbolic Computation 32 (2001) 143\u2013169.","journal-title":"Journal of Symbolic Computation"},{"key":"5118026_CR14","series-title":"Lecture Notes in Computer Science","first-page":"133","volume-title":"Generic Programming \u2013 International Seminar on Generic Programming","author":"S. Schupp","year":"1998","unstructured":"S. Schupp and R. Loos, SuchThat \u2013 generic programming works, in: Generic Programming \u2013 International Seminar on Generic Programming, eds. M. Jazayeri, R. Loos and D. Musser, Lecture Notes in Computer Science, Vol. 1766 (Springer, Berlin, 1998) pp. 133\u2013145."},{"key":"5118026_CR15","first-page":"17","volume":"8","author":"C. Schwarzweller","year":"1999","unstructured":"C. Schwarzweller, The ring of integers, Euclidean rings and modulo integers, Formalized Mathematics 8 (1999) 17\u201322; available by anonymous ftp from http:\/\/mizar.uwb.edu.pl\/JFM\/Vol11\/int_3.html.","journal-title":"Formalized Mathematics"},{"key":"5118026_CR16","volume-title":"Mathematical Logic","author":"J.R. Shoenfield","year":"1967","unstructured":"J.R. Shoenfield, Mathematical Logic (Addison-Wesley, Reading, MA, 1967)."},{"key":"5118026_CR17","volume-title":"Software Engineering","author":"I. Sommerville","year":"1992","unstructured":"I. Sommerville, Software Engineering, 4th edn. (Addison-Wesley, Reading, MA, 1992).","edition":"4th edn."},{"key":"5118026_CR18","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1997","unstructured":"B. Stroustrup, The C++ Programming Language, 3rd edn. (Addison-Wesley, Reading, MA, 1997).","edition":"3rd edn."},{"key":"5118026_CR19","volume-title":"The Mathematica Book","author":"S. Wolfram","year":"1999","unstructured":"S. Wolfram, The Mathematica Book, 4th edn. (Addison-Wesley, Reading, MA, 1999).","edition":"4th edn."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022924032739.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022924032739\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022924032739.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:36:59Z","timestamp":1747546619000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022924032739"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":19,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["5118026"],"URL":"https:\/\/doi.org\/10.1023\/a:1022924032739","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}