Ordinary Differential Equations

swMATH ID: 28798
Software Authors: Fabian Immler; Johannes Hölzl
Description: Ordinary Differential Equations. Session Ordinary-Differential-Equations 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.
Homepage: https://www.isa-afp.org/entries/Ordinary_Differential_Equations.html
Dependencies: Isabelle
Related Software: Isabelle/HOL; Archive Formal Proofs; Kleene Algebra; Algebraic_VCs; Coquelicot; RODES; Lifting; Transfer; HOL; Isabelle; Coq; Binary Multirelations; Isabelle/UTP; Transformer semantics; Quantales; KeYmaera X; Differential_Game_Logic; KAD; Bellerophon; C-CoRN
Cited in: 6 Documents

Citations by Year