Abstract
Formal proofs and global optimisation are two research areas that have been heavily influenced by the arrival of computers. This article aims to bring both further together by formalising a global optimisation method based on Taylor models: a set of functions is represented by a polynomial together with an error bound. The algorithms are implemented in the proof assistant Coq’s term language, with the ultimate goal to obtain formally proven bounds for any multi-variate smooth function in an efficient way. To this end we make use of constructive real numbers, interval arithmetic, and polynomial bounding techniques.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Azarian, M.K.: A076741. In: Sloane, N.J.A. (ed.) The On-Line Encyclopedia of Integer Sequences (2002), www.research.att.com/njas/sequences/
Bertot, Y.: Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs. Technical report (2005)
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. 125, pp. 29–61. Springer, Heidelberg (1968)
Dowek, G., Geser, A., Muñoz, 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)
Euler, L.: Institutiones calculi differentialis (1755)
Gonthier, G.: A computer-checked proof of the Four Colour Theorem Preprint (2005)
Grégoire, B., Thery, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: FLOP 2006. LNCS, Springer, Heidelberg (2006)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings ICFP 2002 (2002)
Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)
Hales, T.C.: A proof of the Kepler Conjecture. Manuscript (2004)
Hansen, E.: Global Optimization Using Interval Analysis. Marcel Dekker, New York (1992)
Makino, K.: Rigorous Analysis of Nonlinear Motion in Particle Accelerators. PhD thesis, Michigan State University, East Lansing, MI, USA, Also MSUCL-1093 (1998)
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–74. SIAM, Philadelphia (1996)
Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. International Journal of Pure and Applied Mathematics 4(4), 379–456 (2003)
Ménissier-Morain, V.: Arithmétique exacte: conception, algorithmique et performances d’une implémentation informatique en précision arbitraire. Phd thesis, Université Paris 7 (1994)
Merlet, J.-P.: Solving the forward kinematics of a gough-type parallel manipulator with interval analysis. International Journal of Robotics Research 23(3), 221–236 (2004)
Moore, R.E.: Automatic error analysis in digital computation. Technical Report LMSD-48421 Lockheed Missiles and Space Co, Palo Alto, CA (1959)
Moore, R.E.: Interval Arithmetic and Automatic Error Analysis in Digital Computing. PhD thesis, Department of Computer Science, Stanford University (1962)
Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)
Nipkow, T., Bauer, G., Schultz, P.: Flyspeck i: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 21–35. Springer, Heidelberg (2006)
Niqui, M.: Formalising Exact Arithmetic: Representations, Algorithms and Proofs, Radboud University Nijmegen. PhD thesis, Radboud University Nijmegen (September 2004)
Obua, S.: Proving bounds for real linear programs in isabelle/hol. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 227–244. Springer, Heidelberg (2005)
O’Connor, R.: A monadic, functional implementation of real numbers Preprint (2005)
Revol, N., Makino, K., Berz, M.: Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY
Schwichtenberg, H.: Constructive analysis with witnesses, Manuscript (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zumkeller, R. (2006). Formal Global Optimisation with Taylor Models. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_35
Download citation
DOI: https://doi.org/10.1007/11814771_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37187-8
Online ISBN: 978-3-540-37188-5
eBook Packages: Computer ScienceComputer Science (R0)