Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
复制标题
DOI：
10.1007/978-3-031-10769-6_42
复制
发表时间：
2022-03
期刊：
影响因子：
--
通讯作者：
James Gallicchio;Yong Kiam Tan;Stefan Mitsch;André Platzer
中科院分区：
文献类型：
--
作者：
James Gallicchio;Yong Kiam Tan;Stefan Mitsch;André Platzer
定理证明器中的定义包为用户提供了定义和组织感兴趣的概念的方法。该系统描述提出了一个新的定义包的混合系统定理证明器KeYmaera X微分动态逻辑（dL）的基础上。该软件包增加了KeYmaera X对用户定义的平滑函数的支持，这些函数的图形可以通过dL公式隐式表征。值得注意的是，这使得可以隐式地将函数（例如指数函数和三角函数）表征为微分方程的解，然后使用dL的微分方程推理原理来证明这些函数的性质。可信度的软件包是通过最低限度地扩展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.