# Differential Equation Invariance Axiomatization

arXiv: https://arxiv.org/abs/1905.13429 · HTML: https://mlsanity.com/paper/1905.13429/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2019.

## Built on by (most cited first, 3 of 3)

- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI](https://mlsanity.com/paper/2406.11563/) (2024)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)

## Abstract (arXiv)

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 for all semianalytic invariants. This parsimonious axiomatization serves as the logical foundation for reasoning about invariants of differential equations. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case.