微分方程存在性与活性证明的公理化方法

本文提出一种利用微分动态逻辑(dL)对常微分方程(ODEs)的存在性与活性进行演绎验证的公理化方法。该方法可证明给定 ODE 的解存在足够长时间,以在离开给定演化域之前到达给定目标区域。诸多细微之处使得离散活性验证技术(如循环变体)向连续情形的推广变得复杂。例如,ODE 解可能在有限时间内爆破,或其朝目标的进展可能收敛于零。这些细微之处在 dL 中通过利用具有完备公理化的 ODE 不变性性质逐步精化 ODE 活性性质来处理。该方法是广泛适用的:本文调研了文献中的若干活性论证,并将其作为 dL 中公理化精化的特例推导出来。这些推导还纠正了所调研文献中的若干可靠性错误,这进一步凸显了 ODE 活性推理的微妙性以及公理化方法的效用。该方法的一个重要特例可推导 ODE 的(全局)存在性性质,而这是每个 ODE 活性论证的基本组成部分。因此,存在性性质及其证明的所有推广可立即导出相应的 ODE 活性论证推广。总体而言,所得到的通用精化步骤库使得既能可靠地开发也能从 dL 公理论证新的 ODE 存在性与活性证明规则。这些见解通过在 KeYmaera X 定理证明器中实现 ODE 活性证明而付诸实践,该证明器用于混合系统。