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.
Type de document :
[Research Report] RR-7228, INRIA. 2010
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
Contributeur : Ioana Pasca <>
Soumis le : mardi 14 décembre 2010 - 16:56:01
Dernière modification le : jeudi 11 janvier 2018 - 16:44:44
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 17:43:56


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers