Computer Science Department
School of Computer Science, Carnegie Mellon University
How to Prove "All" Dfferential Equation Properties
André Platzer, Yong Kiam Tan
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.