KeYmaera X 中的隐式与显式证明管理

混成系统定理证明为信息物理系统交互的离散与连续动态提供了强有力的正确性保证。证明的可信度建立在证明演算的可靠性及其在定理证明器中正确实现的基础之上。以一个被精简至最小限度的可靠性关键核心更容易实现正确性，但作为后果，证明便利性必须在可靠性关键核心之外通过证明管理技术来重新获得。我们提出了构建于 KeYmaera X 可靠性关键核心之上的建模与证明管理技术，以在混成系统证明中支持展开定义、参数化证明、引理及其他有用的证明技术。我们的技术引导 KeYmaera X 中微分动态逻辑证明演算的均匀替换实现，以允许用户选择证明中何时及如何将抽象公式、项或程序展开为其具体定义，以及何时及如何将引理与子证明组合为完整证明。相同技术在隐式子证明（不向用户显式呈现此类子证明）中被利用，以提供证明特性，例如临时隐藏公式，这些特性若在实现于证明器核心中则 notoriously 难以正确实现，但作为核心之外的证明管理技术则变得可信。我们以若干有用证明技术说明我们的方法，并讨论它们在 KeYmaera X 用户界面上的呈现。