×

Numerical analysis of ordinary differential equations in Isabelle/HOL. (English) Zbl 1360.68753

Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 377-392 (2012).
Summary: Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.
We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce generic one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods.
We give an executable specification of the Euler method as an instance of one-step methods. With user-supplied proofs for bounds of the differential equation we can prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.
For the entire collection see [Zbl 1246.68023].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
34-04 Software, source code, etc. for problems pertaining to ordinary differential equations
34A12 Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations
PDF BibTeX XML Cite
Full Text: DOI