{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085177},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569442"},{"type":"electronic","value":"9783540478300"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56944-8_68","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:58:20Z","timestamp":1330257500000},"page":"351-353","source":"Crossref","is-referenced-by-count":2,"title":["Reasoning about the reals: the marriage of HOL and maple"],"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,6,7]]},"reference":[{"key":"32_CR1","unstructured":"R. J. Boulton, On Efficiency in Theorem Provers which Fully Expand Proofs into Primitive Inferences, Technical Report 248, University of Cambridge 1992."},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"D. Clement, A Distributed Architecture for Programming Environment, Proceedings of ACM SIGSOFT'90 SDE-4, Software Engineering Notes, Vol 15, no. 6, Irvine Ca, 1990.","DOI":"10.1145\/99277.99280"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"B. W. Char, K. O. Geddes, G. H. Gonnet, B. L. Leong, M. B. Monagan and S. M. Watt. A Tutorial Introduction to Maple V, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4615-6996-1"},{"key":"32_CR4","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5 (1940) pp. 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR5","unstructured":"M. Gordon, T. Melham, Introduction to HOL, Cambridge University Press 1993."},{"key":"32_CR6","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":"32_CR7","unstructured":"M. Gordon, Private Communication."},{"key":"32_CR8","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":"32_CR9","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."},{"issue":"82","key":"32_CR10","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 7(82), pp. 418\u2013446, 1958.","journal-title":"Czechoslovak Mathematics Journal"},{"key":"32_CR11","volume-title":"Classical and modern integration theories","author":"I. N. Pesin","year":"1970","unstructured":"I. N. Pesin, Classical and modern integration theories, Academic Press, New York 1970."}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56944-8_68.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:04:15Z","timestamp":1713625455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56944-8_68"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569442","9783540478300"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-56944-8_68","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}