Ordinary Differential Equations


Title: Ordinary Differential Equations
Authors: Fabian Immler and Johannes Hölzl
Submission date: 2012-04-26

Session HOL-ODE formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.

Not in the generated document are the following sessions:

  • HOL-ODE-Refinement: Intermediate session combining \texttt{HOL-ODE} and Lammich's (automatic) refinement framework.
  • HOL-ODE-Numerics: Rigorous numerical algorithms for computing enclosures of solutions based on Runge-Kutta methods and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes.
  • HOL-ODE-Examples: Applications of the numerical algorithms to concrete systems of ODEs (e.g., van der Pol and Lorenz attractor).

Change history: [2014-02-13]: added an implementation of the Euler method based on affine arithmetic
[2016-04-14]: added flow and variational equation
[2016-08-03]: numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
  author  = {Fabian Immler and Johannes Hölzl},
  title   = {Ordinary Differential Equations},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2012,
  note    = {\url{http://isa-afp.org/entries/Ordinary_Differential_Equations.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Affine_Arithmetic, Automatic_Refinement, Collections, Refine_Monadic, Show
Used by: Differential_Dynamic_Logic