Formal proofs for theoretical properties of Newton's method

DOI10.1017/S0960129511000077zbMath1264.65080OpenAlexW2154709206MaRDI QIDQ3094171

Ioana Paşca

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000077

zbMATH Keywords

Newton's methodKantorovitch's theoremnumerical algorithm including roundingproof assistant \texttt{Coq}

Mathematics Subject Classification ID

Numerical computation of solutions to systems of equations (65H10)

Related Items (2)

Formally-verified round-off error analysis of Runge-Kutta methods ⋮ A formal study of Bernstein coefficients and polynomials

Uses Software

• ACL2
• Coq
• C-CoRN

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A Skeptic's approach to combining HOL and Maple
• Packaging Mathematical Structures
• Formal Verification of Exact Computations Using Newton’s Method
• Canonical Big Operators
• Real Number Calculations and Theorem Proving
• Certified Exact Transcendental Real Number Computation in Coq
• Nonstandard analysis in ACL2

This page was built for publication: Formal proofs for theoretical properties of Newton's method