紧致初值问题的公理化：未解决的问题

《Journal of the ACM》：Axiomatization of Compact Initial Value Problems: Open Properties

该研究证明了对具有紧集初始条件和时间范围的开放安全性、开放活性和存在性属性的多项式初值问题（IVPs）的公理化系统完备性，提出模块化可计算程序统一符号逻辑与数值分析，生成带微分不变式的符号证明以建立数值解的严格误差界限，适用于有理系数及紧集参数的IVPs，并扩展至非紧集参数情况。

　　

摘要

本文证明了对于具有紧致初始条件和紧致时间范围的初值问题（IVPs），其公理化体系的完备性，这些条件涉及有界开放安全性、开放活性及存在性等属性。完备性使得这些属性的证明能够系统地归结为微分方程不变量的完整公理化问题。该成果通过一种可计算的过程，将符号逻辑与数值分析结合起来，生成包含微分不变量的符号证明，从而为多项式初值问题的数值解提供严格的误差界限。该过程具有模块化特性，适用于所有具有有理系数和初始条件的多项式IVPs，并且符号参数被限制在紧致集合内。此外，本文还讨论了对于初始条件/符号参数不必然受限于紧致集合的IVPs的推广方法，这些推广方法是通过基于该公理化体系推导出完全符号化的公理/证明规则来实现的。