{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:32Z","timestamp":1725551912423},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540314301"},{"type":"electronic","value":"9783540314318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11618027_20","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:48:07Z","timestamp":1137671287000},"page":"299-314","source":"Crossref","is-referenced-by-count":3,"title":["Gr\u00f6bner Bases \u2014 Theory Refinement in the Mizar System"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Bancerek, G.: Reduction Relations; Formalized Mathematics (1995), available in JFM from [Miz05]"},{"issue":"7","key":"20_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S1571-0661(04)80758-8","volume":"85","author":"Grzegorz Bancerek","year":"2003","unstructured":"Bancerek, G.: On the Structure of Mizar Types. In: Geuvers, H., Kamareddine, F. (eds.) Proc. of MLC 2003. ENTCS, vol.\u00a085(7) (2003)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR3","volume-title":"Gr\u00f6bner Bases \u2014 A Computational Approach to Commutative Algebra","author":"T. Becker","year":"1993","unstructured":"Becker, T., Weispfenning, V.: Gr\u00f6bner Bases \u2014 A Computational Approach to Commutative Algebra. Springer, Heidelberg (1993)"},{"key":"20_CR4","unstructured":"Backer, J., Rudnicki, P., Schwarzweller, C.: Ring Ideals; Formalized Mathematics (2000), available in JFM from [Miz05]"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-09519-5_52","volume-title":"Symbolic and Algebraic Computation","author":"B. Buchberger","year":"1979","unstructured":"Buchberger, B.: A Criterion for Detecting Unnecessary Reductions in the Construction of Gr\u00f6bner Bases. In: Ng, K.W. (ed.) EUROSAM 1979 and ISSAC 1979. LNCS, vol.\u00a072, pp. 3\u201321. Springer, Heidelberg (1979)"},{"key":"20_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/CBO9780511565847.003","volume-title":"Gr\u00f6bner Bases and Applications","author":"B. Buchberger","year":"1998","unstructured":"Buchberger, B.: Introduction to Gr\u00f6bner bases. In: Buchberger, B., Winkler, F. (eds.) Gr\u00f6bner Bases and Applications, pp. 3\u201331. Cambridge University Press, Cambridge (1998)"},{"key":"20_CR7","unstructured":"Buchberger, B.: Mathematical Knowledge Management in Theorema. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of the First International Workshop on Mathematical Knowledge Management, Linz, Austria (2001)"},{"key":"20_CR8","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen, \n                    \n                      http:\/\/www.cs.kun.nl\/~freek\/notes\/"},{"key":"20_CR9","volume-title":"Ideals, Varieties and Algorithms","author":"D. Cox","year":"1996","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties and Algorithms, 2nd edn. Springer, New York (1996)","edition":"2"},{"key":"20_CR10","unstructured":"Davies, M.: Obvious Logical Inferences. In: Proceedings of the 7th International Joint Conference on Artificial Intelligence, pp. 530\u2013531 (1981)"},{"key":"20_CR11","first-page":"243","volume-title":"Formal Models and Semantics","author":"Nachum DERSHOWITZ","year":"1990","unstructured":"Dershowitz, N., Jounnaud, J.P.: Rewrite Systems. In: van Leeuven, J. (ed.) Formal Models and Semantics \u2014 Handbook of Theoretical Computer Science, vol.\u00a0B. Elsevier, Amsterdam (1990)"},{"key":"20_CR12","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 - CADE-11","author":"W. Farmer","year":"1992","unstructured":"Farmer, W., Guttman, J., Thayer, F.: Little Theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 567\u2013581. Springer, Heidelberg (1992)"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. Farmer","year":"1993","unstructured":"Farmer, W., Guttman, J., Thayer, F.: IMPS \u2013 An Interactive Mathematical Proof System. Journal of Automated Reasoning\u00a011, 213\u2013248 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-27818-4_10","volume-title":"Mathematical Knowledge Management","author":"A. Grabowski","year":"2004","unstructured":"Grabowski, A., Schwarzweller, C.: Rough Concept Analysis \u2014 Theory Development in the Mizar System. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 130\u2013144. Springer, Heidelberg (2004)"},{"key":"20_CR15","unstructured":"Harrison, J.: Complex Quantifier Elimination in HOL. In: Supplementary Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logic, pp. 159\u2013174 (2001)"},{"key":"20_CR16","unstructured":"Ja\u015bkowski, S.: On the Rules of Suppositon in Formal Logic. Studia Logica\u00a01 (1934)"},{"key":"20_CR17","unstructured":"Lee, G.: Piotr Rudnicki, Dickson\u2019s Lemma; Formalized Mathematics (2002), available in JFM from [Miz05]"},{"key":"20_CR18","unstructured":"The Mizar Home Page, \n                    \n                      http:\/\/mizar.org"},{"key":"20_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-30210-0_15","volume-title":"Artificial Intelligence and Symbolic Computation","author":"J. Medina-Bulo","year":"2004","unstructured":"Medina-Bulo, J., Paloma-Lozano, F., Alonzo-Jim\u00e9nez, J., Ruiz-Reina, J.-L.: Verified Computer Algebra in Acl2. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 171\u2013184. Springer, Heidelberg (2004)"},{"issue":"1\/2","key":"20_CR20","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative Algebra in the Mizar System. Journal of Symbolic Computation\u00a032(1\/2), 143\u2013169 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR21","unstructured":"Rudnicki, P., Trybulec, A.: Multivariate polynomials with arbitrary number of variables; Formalized Mathematics (1999), available in JFM from [Miz05]"},{"key":"20_CR22","unstructured":"Rudnicki, P., Trybulec, A.: Mathematical Knowledge Management in Mizar. In: Buchberger, B., Caprotti, O. (eds.) Proc. of MKM 2001, Linz, Austria (2001)"},{"key":"20_CR23","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. Fundamenta Mathematicae\u00a032, 176\u2013183 (1939)","journal-title":"Fundamenta Mathematicae"},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1026518331905","volume":"26","author":"L. Th\u00e9ry","year":"2001","unstructured":"Th\u00e9ry, L.: A Machine-Checked Implementation of Buchberger\u2019s Algorithm. Journal of Automated Reasoning\u00a026, 107\u2013137 (2001)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11618027_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:06Z","timestamp":1619507526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11618027_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314301","9783540314318"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11618027_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}