Differential Equation Invariance Axiomatization
Andr\'e Platzer, Yong Kiam Tan
TL;DR
This paper establishes a complete logical framework for reasoning about invariants of differential equations, including complex cases described by Noetherian functions, using innovative proof techniques like differential ghosts.
Contribution
It introduces a complete axiomatization for differential equation invariants, leveraging differential ghosts and extending to Noetherian functions for the first time.
Findings
Proves completeness of axiomatization for analytic invariants.
Introduces differential ghosts as a proof technique.
Extends completeness to Noetherian functions.
Abstract
This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis. An extended axiomatization with existence and uniqueness axioms is complete for all local progress properties, and, with a real induction axiom, is complete…
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.