Reseña: Numerical analysis of ordinary differential equations in Isabelle/HOL

El miércoles (15 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle/HOL titulado Numerical analysis of ordinary differential equations in Isabelle/HOL

Sus autores son Fabian Immler y Johannes Hölzl (de la Technische Universität München).

El resumen del trabajo es

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.

El código de la formalización en Isabelle/HOL se encuentra aquí.