微分代数动态逻辑的实解析方法

本文引入了一种用于实解析微分代数动态逻辑的证明演算，能够实现微分代数方程的正确变换。应用包括从微分代数方程到常微分方程的指标约减。该演算确保了微分代数方程证明原理与混合系统的（微分形式）微分动态逻辑之间的兼容性。一个关键贡献是幽灵切换，它建立了将多模态系统分解为混合系统的精确条件，从而正确地实现了复杂微分代数动态的混合化。该演算在欧几里得摆到指标约减形式的等价性证明中得到了演示。