{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:37:03Z","timestamp":1725467823566},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649601"},{"type":"electronic","value":"9783540498162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055902","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T21:17:34Z","timestamp":1154035054000},"page":"55-66","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about coding theory: The benefits we get from computer algebra"],"prefix":"10.1007","author":[{"given":"Clemens","family":"Ballarin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"5_CR1","first-page":"150","volume-title":"Theorems and algorithms: An interface between Isabelle and Maple","author":"C. Ballarin","year":"1995","unstructured":"Clemens Ballarin, Karsten Homann, and Jacques Calmet. Theorems and algorithms: An interface between Isabelle and Maple. In A. H. M. Levelt, editor, ISSAC \u201995: International symposium on symbolic and algebraic computation \u2014 July 1995, Montr\u00e9al, Canada, pages 150\u2013157. ACM Press, 1995."},{"key":"5_CR2","first-page":"22","volume-title":"number 1128 in Lecture Notes in Computer Science","author":"M. Bronstein","year":"1996","unstructured":"Manuel Bronstein. Sumit \u2014 a strongly-typed embeddable computer algebra library. In Calmet and Limongelli [1996], pages 22\u201333."},{"issue":"3\u20134","key":"5_CR3","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1018920108903","volume":"19","author":"J. Calmet","year":"1997","unstructured":"J. Calmet and J. A. Campbell. A perspective on symbolic mathematical computing and artificial intelligence. Annals of Mathematics and Artificial Intelligence, 19(3\u20134):261\u2013277, 1997.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"volume-title":"number 1128 in Lecture Notes in Computer Science","year":"1996","key":"5_CR4","unstructured":"Jacques Calmet and Carla Limongelli, editors. Design and Implementation of Symbolic Computation Systems: International Symposium, DISCO \u201996, Karlsruhe, Germany, September 18\u201320, 1996: proceedings, number 1128 in Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"issue":"1","key":"5_CR5","first-page":"56","volume":"3","author":"E. Clarke","year":"1993","unstructured":"Edmund Clarke and Xudong Zhao. Analytica: A theorem prover for Mathematica. The Mathematica Journal, 3(1):56\u201371, 1993.","journal-title":"The Mathematica Journal"},{"issue":"2","key":"5_CR6","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/235699.235705","volume":"30","author":"R. M. Corless","year":"1996","unstructured":"Robert M. Corless and David J. Jeffrey. The unwinding number. ACM SIGSAM Bulletin, 30(2):28\u201335, 1996.","journal-title":"ACM SIGSAM Bulletin"},{"issue":"3","key":"5_CR7","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/271130.271135","volume":"31","author":"R. M. Corless","year":"1997","unstructured":"R. M. Corless and D. J. Jeffrey. The Turing factorization of a rectangular matrix. ACM SIGSAM Bulletin, 31(3):20\u201328, 1997.","journal-title":"ACM SIGSAM Bulletin"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Keith O. Geddes, Stephen R. Czapor, and George Labahan. Algorithms for Computer Algebra. Kluwer Academic Publishers, 1992.","DOI":"10.1007\/b102438"},{"key":"5_CR9","unstructured":"John Robert Harrison. Theorem proving with the real numbers. Technical Report 408, University of Cambridge, Computer Laboratory, November 1996."},{"key":"5_CR10","volume-title":"Number 150 in Monographs and textbooks in pure and applied mathematics","author":"D. G. Hoffman","year":"1991","unstructured":"D. G. Hoffman, D. A. Leonard, C. C. Lindner, K. T. Phelps, C. A. Rodger, and J. R. Wall. Coding Theory: The Essentials. Number 150 in Monographs and textbooks in pure and applied mathematics. Marcel Dekker, Inc., New York, 1991."},{"key":"5_CR11","volume-title":"Number 152 in Dissertationen zur K\u00fcnstlichen Intelligenz","author":"K. Homann","year":"1997","unstructured":"Karsten Homann. Symbolisches L\u00f6sen mathematischer Probleme durch Kooperation algorithmischer und logischer Systeme. Number 152 in Dissertationen zur K\u00fcnstlichen Intelligenz. infix, St. Augustin, 1997."},{"key":"5_CR12","first-page":"204","volume-title":"number 1128 in Lecture Notes in Computer Science","author":"M. Kerber","year":"1996","unstructured":"Manfred Kerber, Michael Kohlhase, and Volker Sorge. Integrating computer algebra with proof planning. In Calmet and Limongelli [1996], pages 204\u2013215."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: a generic theorem prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"7","key":"5_CR14","first-page":"778","volume":"38","author":"D. R. Stoutemyer","year":"1991","unstructured":"David R. Stoutemyer. Crimes and misdemeanors in the computer algebra trade. Notices of the American Mathematical Society, 38(7):778\u2013785, 1991.","journal-title":"Notices of the American Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055902","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T17:42:26Z","timestamp":1549906946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649601","9783540498162"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0055902","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}