Bachelor Thesis
The interval Newton method is an extension of the well-known Newton’s method for finding roots of differentiable functions. While the latter approximates at most one root of afunction, the interval Newton method finds all roots in a given interval. This method was formalised in Isabelle/HOL using, amongst others, the Approximation package.
The interval Newton method is an extension of the well-known Newton’s method for finding roots of differentiable functions. While the latter approximates at most one root of a function, the interval Newton method finds all roots in a given interval. In this thesis, the method is formalised for arbitrary-precision floating point numbers using the proof assistant Isabelle/HOL. Using the Approximation package, the implementation is easily usable to approximate the roots of a large class of univariate real-valued functions.
Student: Daniel Seidl
Supervisor: Manuel Eberl
Professor: Prof. Tobias Nipkow