Computer Science Department
School of Computer Science, Carnegie Mellon University


How to Prove "All" Dfferential Equation Properties

André Platzer, Yong Kiam Tan

August 2017


Keywords: Differential dynamic logic, algebraic and semialgebraic invariants

This report shows that differential ghosts prove all algebraic invariants of algebraic differential equations by proving that differential radical invariants derive from differential ghosts. Differential ghosts add differential equations to a differential equation system, which, if cleverly chosen, simplify proofs, because they make it possible to relate the change in the quantities of interest to additional variables that can be chosen to evolve freely. A fractional generalization of Darboux's principle for proving invariance of (polynomial) equations along polynomial differential equations is shown to derive from differential ghosts. Differential adjoints are identified as the missing link to derive a vectorial formulation of Darboux's principle from vectorial differential ghosts, from which differential radical invariants follow. These ideas are subsequently generalized from equalities to inequalities, ultimately covering proofs of all true semialgebraic invariants.

40 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by