{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:21Z","timestamp":1725576261439},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232124"},{"type":"electronic","value":"9783540302100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30210-0_15","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:34:36Z","timestamp":1295346876000},"page":"171-184","source":"Crossref","is-referenced-by-count":4,"title":["Verified Computer Algebra in Acl2"],"prefix":"10.1007","author":[{"given":"I.","family":"Medina-Bulo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Palomo-Lozano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. A.","family":"Alonso-Jim\u00e9nez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. L.","family":"Ruiz-Reina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Winkler, F. (eds.): Gr\u00f6bner Bases and Applications. London Mathematical Society Series, vol.\u00a0251 (1998)","DOI":"10.1017\/CBO9780511565847"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/3-540-48167-2_3","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1999","unstructured":"Coquand, T., Persson, H.: Gr\u00f6bner Bases in Type Theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, pp. 33\u201346. Springer, Heidelberg (1999)"},{"key":"15_CR4","volume-title":"Algorithms for Computer Algebra","author":"K.O. Geddes","year":"1998","unstructured":"Geddes, K.O., Czapor, S.R., Labahn, G.: Algorithms for Computer Algebra. Kluwer, Dordrecht (1998)"},{"key":"15_CR5","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)"},{"issue":"2","key":"15_CR6","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning\u00a026(2), 161\u2013203 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-39813-4_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F.J. Mart\u00edn","year":"2003","unstructured":"Mart\u00edn, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz, J.L.: A Formal Proof of Dickson\u2019s Lemma in ACL2. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol.\u00a02850, pp. 49\u201358. Springer, Heidelberg (2003)"},{"key":"15_CR8","unstructured":"Medina, I., Alonso, J.A., Palomo, F.: Automatic Verification of Polynomial Rings Fundamental Properties in ACL2. ACL2 Workshop 2000. Department of Computer Sciences, University of Texas at Austin. TR\u201300\u201329 (2000)"},{"key":"15_CR9","unstructured":"Medina, I., Palomo, F., Alonso, J.A.: Implementation in ACL2 of Well-Founded Polynomial Orderings. In: ACL2 Workshop 2002 (2002)"},{"issue":"1-2","key":"15_CR10","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"},{"issue":"3","key":"15_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1016003314081","volume":"36","author":"J.L. Ruiz","year":"2002","unstructured":"Ruiz, J.L., Alonso, J.A., Hidalgo, M.J., Mart\u00edn, F.J.: Formal Proofs about Rewriting using ACL2. Annals of Mathematics and Artificial Intelligence\u00a036(3), 239\u2013262 (2002)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"15_CR12","unstructured":"Sustyk, M.: Proof of Dickson\u2019s Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping. In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (2003)"},{"issue":"2","key":"15_CR13","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(2), 107\u2013137 (2001)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30210-0_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:49:26Z","timestamp":1605761366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}