{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:56:54Z","timestamp":1740099414188,"version":"3.37.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_11","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"155-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalization of Dub\u00e9\u2019s Degree Bounds for Gr\u00f6bner Bases in Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4378-7854","authenticated-orcid":false,"given":"Alexander","family":"Maletzky","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"11_CR1","volume-title":"An Introduction to Gr\u00f6bner Bases, Graduate Studies in Mathematics","author":"WW Adams","year":"1994","unstructured":"Adams, W.W., Loustaunau, P.: An Introduction to Gr\u00f6bner Bases, Graduate Studies in Mathematics, vol. 3. AMS, Providence (1994)"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"1578","DOI":"10.1016\/j.jpaa.2008.11.022","volume":"213","author":"M Aschenbrenner","year":"2009","unstructured":"Aschenbrenner, M., Leykin, A.: Degree bounds for Gr\u00f6bner bases in algebras of solvable type. J. Pure Appl. Algebra 213, 1578\u20131605 (2009). \n                    https:\/\/doi.org\/10.1016\/j.jpaa.2008.11.022","journal-title":"J. Pure Appl. Algebra"},{"key":"11_CR3","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal. Ph.D. thesis, Mathematisches Institut, Universit\u00e4t Innsbruck, Austria (1965). English translation in J. Symb. Comput. 41(3\u20134), 475\u2013511 (2006)"},{"issue":"4","key":"11_CR4","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1137\/0219053","volume":"19","author":"TW Dub\u00e9","year":"1990","unstructured":"Dub\u00e9, T.W.: The structure of polynomial ideals and Gr\u00f6bner bases. SIAM J. Comput. 19(4), 750\u2013773 (1990). \n                    https:\/\/doi.org\/10.1137\/0219053","journal-title":"SIAM J. Comput."},{"key":"11_CR5","unstructured":"Haftmann, F.: Code Generation from Isabelle\/HOL Theories. \n                    http:\/\/isabelle.in.tum.de\/dist\/Isabelle2018\/doc\/codegen.pdf\n                    \n                  . Part of the Isabelle documentation"},{"key":"11_CR6","unstructured":"Immler, F., Maletzky, A.: Gr\u00f6bner Bases Theory. Archive of Formal Proofs (2016). \n                    http:\/\/isa-afp.org\/entries\/Groebner_Bases.html\n                    \n                  . Formal proof development"},{"key":"11_CR7","unstructured":"Maletzky, A.: Gr\u00f6bner bases and Macaulay matrices in Isabelle\/HOL. Technical report, RISC, Johannes Kepler University Linz, Austria (2018). \n                    http:\/\/www.risc.jku.at\/publications\/download\/risc_5814\/Paper.pdf"},{"key":"11_CR8","unstructured":"Maletzky, A.: Isabelle\/HOL formalization of advanced Gr\u00f6bner bases material (2019). \n                    https:\/\/github.com\/amaletzk\/Isabelle-Groebner\/"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-96812-4_16","volume-title":"Intelligent Computer Mathematics","author":"A Maletzky","year":"2018","unstructured":"Maletzky, A., Immler, F.: Gr\u00f6bner bases of modules and Faug\u00e8re\u2019s \n                    \n                      \n                    \n                    $$F_4$$\n                   algorithm in Isabelle\/HOL. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 178\u2013193. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-96812-4_16"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"EW Mayr","year":"1982","unstructured":"Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305\u2013329 (1982). \n                    https:\/\/doi.org\/10.1016\/0001-8708(82)90048-2","journal-title":"Adv. Math."},{"key":"11_CR11","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"11_CR12","unstructured":"Sternagel, C., Thiemann, R., Maletzky, A., Immler, F.: Executable multivariate polynomials. Archive of Formal Proofs (2010). \n                    http:\/\/isa-afp.org\/entries\/Polynomials.html\n                    \n                  . Formal proof development"},{"key":"11_CR13","unstructured":"Wenzel, M.: The Isabelle\/ISAR Reference Manual (2018). \n                    https:\/\/isabelle.in.tum.de\/dist\/Isabelle2018\/doc\/isar-ref.pdf\n                    \n                  . Part of the Isabelle documentation"},{"key":"11_CR14","unstructured":"Wiesinger-Widi, M.: Gr\u00f6bner bases and generalized sylvester matrices. Ph.D. thesis, RISC, Johannes Kepler University Linz, Austria (2015). \n                    http:\/\/epub.jku.at\/obvulihs\/content\/titleinfo\/776913"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:04:45Z","timestamp":1562036685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}