The Flow of ODEs

DOI10.1007/978-3-319-43144-4_12zbMath1468.68324OpenAlexW2483648716MaRDI QIDQ2829258

Christoph Traut, Fabian Immler

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_12

Mathematics Subject Classification ID

Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations (34A12) Geometric methods in ordinary differential equations (34A26) Dynamics induced by flows and semiflows (37C10) Numerical methods for initial value problems involving ordinary differential equations (65L05) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (7)

A verified ODE solver and the Lorenz attractor ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ A formally verified proof of the central limit theorem ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Verified interactive computation of definite integrals

Uses Software

• Transfer
• Lifting
• RODES
• Unnamed Item
• Unnamed Item

Cites Work

• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• A rigorous ODE solver and Smale's 14th problem
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

This page was built for publication: The Flow of ODEs