Ordinary Differential Equations swMATH ID: 28798 Software Authors: Immler, Fabian; Hölzl, Johannes 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 all top 5 Cited by 6 Authors 4 Immler, Fabian 2 Huerta y Munive, Jonathan Julián 2 Struth, Georg 1 Foster, Simon 1 Hölzl, Johannes 1 Traut, Christoph Cited in 1 Serial 3 Journal of Automated Reasoning Cited in 5 Fields 6 Computer science (68-XX) 4 Ordinary differential equations (34-XX) 3 Dynamical systems and ergodic theory (37-XX) 3 Numerical analysis (65-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year