论文标题
带有微分方程的隐式定义keymaera X（系统描述）
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
论文作者
论文摘要
定理掠夺中的定义软件包为用户提供了定义和组织感兴趣概念的方法。此系统描述基于差分动态逻辑（DL）提供了一个新的定义软件包keymaera x。该软件包添加了Keymaera X支持用户定义的平滑功能，其图形可以隐含地以DL公式为特征。值得注意的是，这使得可以隐式将函数（例如指数和三角函数）作为微分方程的解决方案，然后使用DL的微分方程推理原理证明这些函数的属性。包装的可信赖性是通过最小化的Keymaera X使用单个公理方案扩展了keymaera X的重要性核心来实现的，该方案可以通过其隐式表征扩展功能出现。为用户提供了一个高级界面，用于定义功能和非功能性策略，该函数对混合系统证明中隐式特征的低级推理自动化。
Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for user-defined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably, this makes it possible to implicitly characterize functions, such as the exponential and trigonometric functions, as solutions of differential equations and then prove properties of those functions using dL's differential equation reasoning principles. Trustworthiness of the package is achieved by minimally extending KeYmaera X's soundness-critical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a high-level interface for defining functions and non-soundness-critical tactics that automate low-level reasoning over implicit characterizations in hybrid system proofs.
