一句话：证明微分动态逻辑的微分方程公理对所有代数不变式完备，并用微分幽灵构造证明。
论文研究微分方程不变式的公理化完备性。作者证明微分动态逻辑（dL）中关于微分方程的公理对于所有代数不变式都是完备的，即任何此类代数不变式都可由该公理系统推出。证明的关键方法是引入“微分幽灵”（differential ghosts）：沿新微分方程自由演化的附加变量。巧妙选择的微分幽灵如同暗物质，可构造新的假设状态，使其与原状态变量的关系满足此前不存在的不变式；再将这些新不变式反射回原系统，从而完成对原系统的分析。该结果为微分不变式推理提供了完备的证明论基础。
We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof 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.
DOI 原文 ·
@inproceedings{paperbot4380,
title = {Differential Equation Axiomatization},
author = {André Platzer and Yong Kiam Tan},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209147}
}