Formalization of Function Matrix Theory in HOL
Formalization of Function Matrix Theory in HOL
复制标题
HOL 中函数矩阵理论的形式化
DOI：
10.1155/2014/201214
复制
发表时间：
2014-07
影响因子：
--
通讯作者：
Wei Hongxing
中科院分区：
文献类型：
--
作者：
Guan Yong;Ye Shiwei;Zhang Jie;Wei Hongxing
函数矩阵，其中的元素是函数而不是数字，被广泛应用于动态系统的模型分析，如控制系统和机器人。在安全关键型应用中，需要对动态系统进行正式和准确的分析，以确保其正确性和安全性。高阶逻辑定理证明是满足这一要求的一种很有前途的技术。本文利用HOL定理证明器提出了函数向量和函数矩阵理论的高阶逻辑形式化，包括数据类型、运算及其性质，并进一步给出了函数向量和函数矩阵的微分和积分的形式化。形式化在HOL系统中以库的形式实现。以二次函数微分的形式化分析为例，说明了所提出的形式化方法的有效性。
Function matrices, in which elements are functions rather than numbers, are widely used in model analysis of dynamic systems such as control systems and robotics. In safety-critical applications, the dynamic systems are required to be analyzed formally and accurately to ensure their correctness and safeness. Higher-order logic (HOL) theorem proving is a promise technique to match the requirement. This paper proposes a higher-order logic formalization of the function vector and the function matrix theories using the HOL theorem prover, including data types, operations, and their properties, and further presents formalization of the differential and integral of function vectors and function matrices. The formalization is implemented as a library in the HOL system. A case study, a formal analysis of differential of quadratic functions, is presented to show the usefulness of the proposed formalization.
登录
查看更多内容
影响因子：
1.2
作者：
Steven Obua;T. Nipkow
通讯作者：
Steven Obua;T. Nipkow
DOI：
10.1145/307988.307989
发表时间：
1999-04
期刊：
ACM Trans. Design Autom. Electr. Syst.
影响因子：
--
作者：
Christoph Kern;M. Greenstreet
通讯作者：
Christoph Kern;M. Greenstreet
用于表示和推理动作的一系列动态描述逻辑
DOI：
10.1007/s10817-010-9210-1
发表时间：
2012-06
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Liang Chang;Zhongzhi Shi;Tianlong Gu;Lingzhong Zhao
通讯作者：
Lingzhong Zhao
DOI：
10.1007/11541868_8
发表时间：
2005-08
期刊：
--
影响因子：
--
作者：
J. Harrison
通讯作者：
J. Harrison
DOI：
10.1007/11541868_15
发表时间：
2005-08
期刊：
--
影响因子：
--
作者：
Steven Obua
通讯作者：
Steven Obua