{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:14:29Z","timestamp":1737609269298,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_8","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"112-126","source":"Crossref","is-referenced-by-count":5,"title":["VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up"],"prefix":"10.1007","author":[{"given":"A. A.","family":"Adams","sequence":"first","affiliation":[]},{"given":"H.","family":"Gottliebsen","sequence":"additional","affiliation":[]},{"given":"S. A.","family":"Linton","sequence":"additional","affiliation":[]},{"given":"U.","family":"Martin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin. A Verifiable Symbolic Definite Integral Table Look-Up. Technical Report CS\/99\/3, University of St Andrews, 1999.","key":"8_CR1","DOI":"10.1007\/3-540-48660-7_8"},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 97)","year":"1997","unstructured":"E. Brinksma, editor. Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 97). Springer-Verlag LNCS 1217, 1997."},{"key":"8_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03386-9","volume-title":"Symbolic integration I","author":"M. Bronstein","year":"1997","unstructured":"M. Bronstein. Symbolic integration I. Springer-Verlag, Berlin, 1997. Transcendental functions."},{"doi-asserted-by":"crossref","unstructured":"C. W. Brown. Simplification of truth-invariant cylindrical algebraic decompositions. In Gloor [Glo98], pages 295\u2013301.","key":"8_CR4","DOI":"10.1145\/281508.281652"},{"doi-asserted-by":"crossref","unstructured":"A. Bundy, editor. CADE-12: 12th International Conference on Automated Deduction: Proceedings. Springer-Verlag LNAI 814, 1994.","key":"8_CR5","DOI":"10.1007\/3-540-58156-1"},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Integrating Symbolic Mathematical Computation and Artificial Intelligence","year":"1994","unstructured":"J. Calmet and J. A. Campbell, editors. Integrating Symbolic Mathematical Computation and Artificial Intelligence. Springer-Verlag LNCS 958, 1994."},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO\u201996","year":"1996","unstructured":"J. Calmet and C. Limongelli, editors. Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO\u201996. Springer-Verlag LNCS 1128, 1996."},{"key":"8_CR8","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1007\/3-540-58156-1_55","volume-title":"Automated Deduction \u2014 CADE-12","author":"Edmund Clarke","year":"1994","unstructured":"E. Clarke and X. Zhao. Combining symbolic computation and theorem proving: Some problems of Ramanujan. In Bundy [Bun94], pages 758\u2013763."},{"unstructured":"J. H. Davenport. Really Strong Integration Algorithms. In preparation. dB80. N. G. de Bruijn. A Survey of the Project AUTOMATH. In Seldin and Hindley [SH80], pages 579\u2013606.","key":"8_CR9"},{"unstructured":"S. Dalmas, M. Ga\u00ebtano, and C. Huchet. A Deductive Database for Mathematical Formulas. In Calmet and Limongelli [CL96].","key":"8_CR10"},{"doi-asserted-by":"crossref","unstructured":"S. Dalmas, M. Ga\u00ebtano, and S. Watt. An OpenMath 1.0 Implementation. In K\u00fcchlin [K\u00fcc97], pages 241\u2013248.","key":"8_CR11","DOI":"10.1145\/258726.258794"},{"key":"8_CR12","volume-title":"Computer algebra","author":"J. H. Davenport","year":"1993","unstructured":"J. H. Davenport, Y. Siret, and E. Tournier. Computer algebra. Academic Press Ltd, London, second edition, 1993.","edition":"second edition"},{"unstructured":"B. Dup\u00e9e. Using Computer Algebra to Find Singularities of Elementary Real Functions. Available from the author, bjd@maths.bath.ac.uk, 1998.","key":"8_CR13"},{"unstructured":"B. Dutertre. Elements of Mathematical Analysis in PVS. In von Wright et al. [vWGH96].","key":"8_CR14"},{"doi-asserted-by":"crossref","unstructured":"T. Einwohner and R. J. Fateman. Searching techniques for Integral Tables. In Levelt [Lev95], pages 133\u2013139.","key":"8_CR15","DOI":"10.1145\/220346.220364"},{"unstructured":"R. J. Fateman and T. Einwohner. TILU Table of Integrals Look Up. Web Service. http:\/\/http.cs.berkeley.edu\/~fateman\/htest.html . 126 A. A. Adams et al.","key":"8_CR16"},{"doi-asserted-by":"crossref","unstructured":"J. Fleuriot and L. Paulson. A combination of nonstandard analysis and geometry theorem proving with application to Newton\u2019s Principia. In Kirchner and Kirchner [KK98], pages 3\u201316.","key":"8_CR17","DOI":"10.1007\/BFb0054241"},{"key":"8_CR18","volume-title":"Integraltafel","author":"W. Gro\u00ebbner","year":"1961","unstructured":"W. Gro\u00ebbner and N. Hofreiter. Integraltafel. Springer-Verlag, Vienna, 1961."},{"unstructured":"O. Gloor, editor. Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation. ACM Press, 1998.","key":"8_CR19"},{"doi-asserted-by":"crossref","unstructured":"J. Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998.","key":"8_CR20","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-60156-2_3","volume-title":"Integrating Symbolic Mathematical Computation and Artificial Intelligence","author":"Karsten Homann","year":"1995","unstructured":"K. Homann and J. Calmet. Combining theorem proving and symbolic mathematical computing. In Calmet and Campbell [CC94], pages 18\u201329."},{"key":"8_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0484-5","volume-title":"Introduction to Maple","author":"A. Heck","year":"1996","unstructured":"A. Heck. Introduction to Maple. Springer-Verlag, New York, second edition, 1996.","edition":"second edition"},{"key":"8_CR23","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/3-540-57826-9_134","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"John Harrison","year":"1994","unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Joyce and Seger [JS94], pages 174\u2013185."},{"doi-asserted-by":"crossref","unstructured":"R. D. Jenks and R. S. Sutor. AXIOM. Springer-Verlag, 1992.","key":"8_CR24","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"8_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Higher order logic theorem proving and its applications","year":"1994","unstructured":"J. J. Joyce and C-J. H. Seger, editors. Higher order logic theorem proving and its applications, Berlin, 1994. Springer-Verlag LNCS 780."},{"key":"8_CR26","first-page":"31","volume":"18","author":"M. Klerer","year":"1968","unstructured":"M. Klerer and F. Grossman. Error Rates in Tables of Indefinite Integrals. Journal of the Industrial Mathematics Society, 18:31\u201362, 1968.","journal-title":"Journal of the Industrial Mathematics Society"},{"doi-asserted-by":"crossref","unstructured":"KK98. C. Kirchner and H. Kirchner, editors. CADE-15: 15th International Conference on Automated Deduction: Proceedings. Springer-Verlag LNAI 1421, 1998.","key":"8_CR27","DOI":"10.1007\/BFb0054239"},{"unstructured":"M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra with Proof Planning. In Calmet and Limongelli [CL96].","key":"8_CR28"},{"unstructured":"W. W. K\u00fcchlin, editor. Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation. ACM Press, 1997.","key":"8_CR29"},{"key":"8_CR30","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 6th International Symposium on Symbolic and Algebraic Computation, ISSAC\u2019 95","year":"1995","unstructured":"A. H. M. Levelt, editor. Proceedings of the 6th International Symposium on Symbolic and Algebraic Computation, ISSAC\u2019 95. Springer-Verlag LNCS 1004, 1995."},{"doi-asserted-by":"crossref","unstructured":"U. Martin. Computers, Reasoning and Mathematical Practice. In Computational Logic, NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., 1998.","key":"8_CR31","DOI":"10.1007\/978-3-642-58622-4_9"},{"key":"8_CR32","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0035400","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Sam Owre","year":"1997","unstructured":"S. Owre, J. Rushby, and N. Shankar. Integration in PVS: Tables, Types, and Model Checking. In Brinksma [Bri97], pages 366\u2013383."},{"unstructured":"J. P. Seldin and J. R. Hindley, editors. To H.B. Curry: essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980.","key":"8_CR33"},{"key":"8_CR34","first-page":"779","volume":"38","author":"D. Stoutemyer","year":"1991","unstructured":"D. Stoutemyer. Crimes and misdemeanours in the computer algebra trade. Notices of the AMS, 38:779\u2013785, 1991.","journal-title":"Notices of the AMS"},{"doi-asserted-by":"crossref","unstructured":"L. Th\u00e9ry. A Certified Version of Buchberger\u2019s Algorithm. In Kirchner and Kirchner [KK98], pages 349\u2013364.","key":"8_CR35","DOI":"10.1007\/BFb0054271"},{"key":"8_CR36","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"A. Trybulec. The Mizar-QC 6000 logic information language. ALCC Bulletin, 6:136\u2013140, 1978.","journal-title":"ALCC Bulletin"},{"key":"8_CR37","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference","year":"1996","unstructured":"J. von Wright, J. Grundy, and J. Harrison, editors. Theorem Proving in Higher Order Logics: 9th International Conference. Springer-Verlag LNCS 1125, 1996."},{"unstructured":"Wolfram Research Inc. The integrator: the power to do integrals as the world has never seen before, http:\/\/www.integrals.com .","key":"8_CR38"},{"key":"8_CR39","volume-title":"CRC standard mathematical tables and formulae","year":"1996","unstructured":"D. Zwillinger, S. G. Krantz, and K. H. Rosen, editors. CRC standard mathematical tables and formulae. CRC Press, Boca Raton, FL, 30th edition, 1996.","edition":"30th edition"},{"unstructured":"D. Zwillinger. Standard Math Interactive. CD-ROM, 1998.","key":"8_CR40"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:55:23Z","timestamp":1737525323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}