This repository contains a formalization of Differential Dynamic Logic (dL) in the Lean 4 proof assistant. It formalizes the syntax, static and dynamic semantics of dL, as well as Uniform Substitution, and includes proofs of the ODE axioms.
| Name | Name | Last commit date | ||
|---|---|---|---|---|
This repository contains a formalization of Differential Dynamic Logic (dL) in the Lean 4 proof assistant. It formalizes the syntax, static and dynamic semantics of dL, as well as Uniform Substitution, and includes proofs of the ODE axioms.