{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:14Z","timestamp":1763467874637},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_2","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"2-17","source":"Crossref","is-referenced-by-count":20,"title":["Proving Bounds on Real-Valued Functions with Computations"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Melquiond","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11814771_36","volume-title":"Automated Reasoning","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L.: A purely functional library for modular arithmetic and its application to certifying large prime numbers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 423\u2013437. Springer, Heidelberg (2006)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11737414_8","volume-title":"Functional and Logic Programming","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L., Werner, B.: A computational approach to Pocklington certificates in type theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 97\u2013113. Springer, Heidelberg (2006)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Mathematical Structure in Computer Sciences 17(1) (2007)","DOI":"10.1017\/S096012950600586X"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Floating point verification in HOL light: The exponential function. In: Algebraic Methodology and Software Technology, 246\u2013260 (1997)","DOI":"10.1007\/BFb0000475"},{"key":"2_CR6","unstructured":"Akbarpour, B., Paulson, L.C.: Towards automatic proofs of inequalities involving elementary functions. In: Cook, B., Sebastiani, R. (eds.) PDPAR: Pragmatics of Decision Procedures in Automated Reasoning, pp. 27\u201337 (2006)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/11541868_13","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Mu\u00f1oz","year":"2005","unstructured":"Mu\u00f1oz, C., Lester, D.: Real number calculations and theorem proving. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 195\u2013210. Springer, Heidelberg (2005)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Daumas, M., Melquiond, G., Mu\u00f1oz, C.: Guaranteed proofs using interval arithmetic. In: Montuschi, P., Schwarz, E. (eds.) Proceedings of the 17th IEEE Symposium on Computer Arithmetic, Cape Cod, MA, USA, pp. 188\u2013195 (2005)","DOI":"10.1109\/ARITH.2005.25"},{"key":"2_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11814771_35","volume-title":"Automated Reasoning","author":"R. Zumkeller","year":"2006","unstructured":"Zumkeller, R.: Formal global optimisation with Taylor models. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 408\u2013422. Springer, Heidelberg (2006)"},{"issue":"2","key":"2_CR10","first-page":"9","volume":"22","author":"D. Stevenson","year":"1987","unstructured":"Stevenson, D., et al.: An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices\u00a022(2), 9\u201325 (1987)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR11","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970906","volume-title":"Methods and Applications of Interval Analysis","author":"R.E. Moore","year":"1979","unstructured":"Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)"},{"key":"2_CR12","volume-title":"Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics","author":"L. Jaulin","year":"2001","unstructured":"Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics. Springer, Heidelberg (2001)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library of floating-point numbers and its application to exact computing. In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 169\u2013184 (2001)","DOI":"10.1007\/3-540-44755-5_13"},{"key":"2_CR14","unstructured":"Boldo, S.: Preuves formelles en arithm\u00e9tiques \u00e0 virgule flottante. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon (2004)"},{"key":"2_CR15","unstructured":"Melquiond, G.: De l\u2019arithm\u00e9tique d\u2019intervalles \u00e0 la certification de programmes. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon, Lyon, France (2006)"},{"key":"2_CR16","unstructured":"Spiwack, A.: Ajouter des entiers machine \u00e0 Coq. Technical report (2006)"},{"key":"2_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Theoretical Aspects of Computer Software, pp. 515\u2013529 (1997)","DOI":"10.1007\/BFb0014565"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:10Z","timestamp":1605762910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}