×

Ordinary Differential Equations

swMATH ID: 28798
Software Authors:
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; Coq; RODES; Lifting; Transfer; HOL; Isabelle; Binary Multirelations; Isabelle/UTP; KeYmaera X; Bellerophon; Transformer semantics; Quantales; Differential_Game_Logic; KAD; C-CoRN
Cited in: 6 Documents

Citations by Year