Formal Proofs for Theoretical Properties of Newton's Method

Ioana Pasca 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suit the features of a proof assistant, and designing new proofs based on the existing ones to deal with optimizations of the method. We start from Kantorovitch's theorem that states the convergence of Newton's method in the case of a system of equations. To formalize this proof inside the proof assistant Coq we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.
Document type :
Liste complète des métadonnées

Cited literature [25 references]  Display  Hide  Download
Contributor : Ioana Pasca <>
Submitted on : Tuesday, December 14, 2010 - 4:56:01 PM
Last modification on : Thursday, January 11, 2018 - 4:44:44 PM
Document(s) archivé(s) le : Friday, December 2, 2016 - 5:43:56 PM


Files produced by the author(s)


  • HAL Id : inria-00463150, version 2



Ioana Pasca. Formal Proofs for Theoretical Properties of Newton's Method. [Research Report] RR-7228, INRIA. 2010. ⟨inria-00463150v2⟩



Record views


Files downloads