{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T12:53:32Z","timestamp":1776689612319,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_35","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"408-422","source":"Crossref","is-referenced-by-count":12,"title":["Formal Global Optimisation with Taylor Models"],"prefix":"10.1007","author":[{"given":"Roland","family":"Zumkeller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"Azarian, M.K.: A076741. In: Sloane, N.J.A. (ed.) The On-Line Encyclopedia of Integer Sequences (2002), www.research.att.com\/njas\/sequences\/"},{"key":"35_CR2","unstructured":"Bertot, Y.: Calcul de formules affines et de s\u00e9ries enti\u00e8res en arithm\u00e9tique exacte avec types co-inductifs. Technical report (2005)"},{"key":"35_CR3","series-title":"LNM","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Proceedings of the Symposium on Automatic Demonstration","author":"N.G. Bruijn de","year":"1968","unstructured":"de Bruijn, N.G.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Laudet, M. (ed.) Proceedings of the Symposium on Automatic Demonstration, Versailles, France, December 1968. LNM, vol.\u00a0125, pp. 29\u201361. Springer, Heidelberg (1968)"},{"key":"35_CR4","unstructured":"Dowek, G., Geser, A., Mu\u00f1oz, C.: Tactical conflict detection and resolution in a 3-D airspace. In: Proceedings of the 4th USA\/Europe Air Traffic Management R&DSeminar, ATM 2001, Santa Fe, New Mexico (2001)"},{"key":"35_CR5","unstructured":"Euler, L.: Institutiones calculi differentialis (1755)"},{"key":"35_CR6","unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem Preprint (2005)"},{"key":"35_CR7","series-title":"LNCS","volume-title":"FLOP 2006","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Thery, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: FLOP 2006. LNCS, Springer, Heidelberg (2006)"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings ICFP 2002 (2002)","DOI":"10.1145\/581478.581501"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Hales, T.C.: A proof of the Kepler Conjecture. Manuscript (2004)","DOI":"10.1007\/978-3-540-30142-4_9"},{"key":"35_CR11","volume-title":"Global Optimization Using Interval Analysis","author":"E. Hansen","year":"1992","unstructured":"Hansen, E.: Global Optimization Using Interval Analysis. Marcel Dekker, New York (1992)"},{"key":"35_CR12","unstructured":"Makino, K.: Rigorous Analysis of Nonlinear Motion in Particle Accelerators. PhD thesis, Michigan State University, East Lansing, MI, USA, Also MSUCL-1093 (1998)"},{"key":"35_CR13","first-page":"63","volume-title":"Computational Differentiation: Techniques, Applications, and Tools","author":"K. Makino","year":"1996","unstructured":"Makino, K., Berz, M.: Remainder differential algebras and their applications. In: Berz, M., Bischof, C., Corliss, G., Griewank, A. (eds.) Computational Differentiation: Techniques, Applications, and Tools, pp. 63\u201374. SIAM, Philadelphia (1996)"},{"issue":"4","key":"35_CR14","first-page":"379","volume":"4","author":"K. Makino","year":"2003","unstructured":"Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. International Journal of Pure and Applied Mathematics\u00a04(4), 379\u2013456 (2003)","journal-title":"International Journal of Pure and Applied Mathematics"},{"key":"35_CR15","unstructured":"M\u00e9nissier-Morain, V.: Arithm\u00e9tique exacte: conception, algorithmique et performances d\u2019une impl\u00e9mentation informatique en pr\u00e9cision arbitraire. Phd thesis, Universit\u00e9 Paris 7 (1994)"},{"issue":"3","key":"35_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1177\/0278364904039806","volume":"23","author":"J.-P. Merlet","year":"2004","unstructured":"Merlet, J.-P.: Solving the forward kinematics of a gough-type parallel manipulator with interval analysis. International Journal of Robotics Research\u00a023(3), 221\u2013236 (2004)","journal-title":"International Journal of Robotics Research"},{"key":"35_CR17","unstructured":"Moore, R.E.: Automatic error analysis in digital computation. Technical Report LMSD-48421 Lockheed Missiles and Space Co, Palo Alto, CA (1959)"},{"key":"35_CR18","unstructured":"Moore, R.E.: Interval Arithmetic and Automatic Error Analysis in Digital Computing. PhD thesis, Department of Computer Science, Stanford University (1962)"},{"key":"35_CR19","volume-title":"Interval Analysis","author":"R.E. Moore","year":"1966","unstructured":"Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)"},{"key":"35_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/11814771_4","volume-title":"Automated Reasoning","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck i: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 21\u201335. Springer, Heidelberg (2006)"},{"key":"35_CR21","unstructured":"Niqui, M.: Formalising Exact Arithmetic: Representations, Algorithms and Proofs, Radboud University Nijmegen. PhD thesis, Radboud University Nijmegen (September 2004)"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11541868_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Obua","year":"2005","unstructured":"Obua, S.: Proving bounds for real linear programs in isabelle\/hol. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 227\u2013244. Springer, Heidelberg (2005)"},{"key":"35_CR23","unstructured":"O\u2019Connor, R.: A monadic, functional implementation of real numbers Preprint (2005)"},{"key":"35_CR24","unstructured":"Revol, N., Makino, K., Berz, M.: Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY"},{"key":"35_CR25","unstructured":"Schwichtenberg, H.: Constructive analysis with witnesses, Manuscript (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:35Z","timestamp":1605644075000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11814771_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}