Differential Equation Invariance Axiomatization
Differential Equation Invariance Axiomatization
复制标题
DOI：
10.1145/3380825
复制
发表时间：
2020-04-01
影响因子：
2.5
通讯作者：
Tan, Yong Kiam
中科院分区：
文献类型：
--
作者：
Platzer, Andre;Tan, Yong Kiam
本文证明了微分方程不变量用诺特函数描述的公理化的完备性。首先，证明了微分动态逻辑的微分方程公理对于解析不变量的推理是完备的。完备性关键地利用了微分鬼，它引入了额外的变量，可以选择这些变量沿着沿着新的微分方程自由地演化。巧妙选择的微分鬼是暗物质的证明理论对应物。它们创建了一个新的假设状态，其与原始状态变量的关系满足以前不存在的不变量。这些新的不变量在原系统中的反映，然后使其analysis.A扩展公理化的存在性和唯一性公理是完整的所有本地的进展性质，并与真实的归纳公理，是完整的所有半解析不变量。这种简约的公理化作为推理微分方程不变量的逻辑基础。事实上，正是这种逻辑处理使得完备性能够推广到诺特情形。
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 a 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.