{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:25:17Z","timestamp":1761675917754},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_134","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:42Z","timestamp":1330262802000},"page":"174-184","source":"Crossref","is-referenced-by-count":20,"title":["Extending the HOL theorem prover with a computer algebra system to reason about the reals"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"14_CR1","unstructured":"M. Archer, G. Fink, L. Yang, Linking Other Theorem Provers to HOL Using PM: Proof Manager, Proceedings of the 1992 International Workshop on the HOL Theorem Proving System and its Applications, North-Holland 1993."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"R. J. Boulton, A Lazy Approach to Fully-Expansive Theorem Proving, Proceedings of the 1992 International Workshop on the HOL Theorem Proving System and its Applications, North-Holland 1993.","DOI":"10.1016\/B978-0-444-89880-7.50008-5"},{"key":"14_CR3","doi-asserted-by":"crossref","first-page":"195","DOI":"10.2307\/44151511","volume":"5","author":"P. Bullen","year":"1980","unstructured":"P. Bullen, Non-absolute integrals: A survey, Real Analysis Exchange, vol. 5 pp. 195\u2013259, 1980.","journal-title":"Real Analysis Exchange"},{"key":"14_CR4","unstructured":"J. C. Burkill, The Lebesgue Integral, Cambridge Tracts in Mathematics and Mathematical Physics no. 44, Cambridge University Press 1965."},{"key":"14_CR5","volume-title":"LNCS 509","author":"D. Cl\u00e9ment","year":"1991","unstructured":"D. Cl\u00e9ment, F. Montagnac, V. Prunet, Integrated Software Components: a Paradigm for Control Integration, Proceedings of the European Symposium on Software Development Environments and CASE Technology, K\u00f6nigwinter, Springer-Verlag LNCS 509, June 1991."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"B. W. Char, K. O. Geddes, G. H. Gonnet, B. L. Leong, M. B. Monagan, S. M. Watt, A Tutorial Introduction to Maple V, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4615-6996-1"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"D. van Dalen, A. F. Monna, Sets and Integration: an Outline of the Development, Wolters-Noordhoff 1972.","DOI":"10.1007\/978-94-010-2718-2"},{"key":"14_CR8","unstructured":"J. DePree, C. Swartz, Introduction to Real Analysis, Wiley 1988."},{"key":"14_CR9","unstructured":"M. Gordon, Private Communication."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"J. R. Harrison, Constructing the Real Numbers in HOL, Proceedings of the 1992 International Workshop on the HOL Theorem Proving System and its Applications, North-Holland 1993.","DOI":"10.1016\/B978-0-444-89880-7.50016-4"},{"key":"14_CR11","doi-asserted-by":"crossref","first-page":"79","DOI":"10.4153\/CJM-1968-010-5","volume":"20","author":"R. Henstock","year":"1968","unstructured":"R. Henstock, A Riemann-type integral of Lebesgue power, Canadian Journal of Mathematics vol. 20 pp. 79\u201387, 1968.","journal-title":"Canadian Journal of Mathematics"},{"key":"14_CR12","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198535669.001.0001","volume-title":"The General Theory of Integration","author":"R. Henstock","year":"1991","unstructured":"R. Henstock, The General Theory of Integration, Clarendon Press, Oxford 1991."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"R. D. Jenks, R. S. Sutor, AXIOM: the Scientific Computation System, Springer-Verlag 1992.","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"N. Kajler, Cas\/Pi: A Portable and Extensible Interface for Computer Algebra Systems, Proceedings of ISSAC '92, ACM 1992.","DOI":"10.1145\/143242.143359"},{"key":"14_CR15","unstructured":"A. Kechris, The Complexity of Antidifferentiation, Denjoy Totalization, and Hyperarithmetic Reals, Proceedings of the International Conference of Mathematicians, Berkeley 1986."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"R. Kumar, T. Kropf, K. Schneider, Integrating a First-Order Automatic Prover in the HOL environment, Proceeding of the 1991 International Workshop on the HOL Theorem Prover System and its Applications, IEEE Computer Society Press 1991.","DOI":"10.1109\/HOL.1991.596284"},{"issue":"82","key":"14_CR17","first-page":"418","volume":"7","author":"J. Kurzweil","year":"1958","unstructured":"J. Kurzweil, Generalized Ordinary Differential Equations and Continuous Dependence on a Parameter, Czechoslovak Mathematics Journal vol. 7(82), pp. 418\u2013446, 1958.","journal-title":"Czechoslovak Mathematics Journal"},{"key":"14_CR18","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1080\/00029890.1973.11993291","volume":"80","author":"E. J. McShane","year":"1973","unstructured":"E. J. McShane, A Unified Theory of Integration, American Mathematical Monthly 80 pp. 349\u2013357, 1973.","journal-title":"American Mathematical Monthly"},{"key":"14_CR19","unstructured":"I. N. Pesin, Classical and modern integration theories, Academic Press 1970."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"C. Seger, J. J. Joyce, A Two-level Formal Verification Methodology using HOL and COSMOS, Technical Report 91-10, Department of Computer Science, University of British Columbia, 1991.","DOI":"10.1007\/3-540-55179-4_29"},{"key":"14_CR21","unstructured":"S. Wolfram, Mathematica, A System for Doing Mathematics by Computer, Addison-Wesley 1988."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_134.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:32:50Z","timestamp":1713627170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_134","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}