DART XII

Kassel (Germany) April 9^{th} - 12^{th} 2024

XII. Conference on Differential Algebra and Related Topics

April 9^{th} - 12^{th} 2024

Kassel University, Germany

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 where properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case. Moreover, the approach is purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.

This talk is based on joint work with Yong Kiam Tan, LICS 2018, JACM 2020.