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í.