函数矩阵理论在HOL4中的形式化  

Formalization of Function Matrix Theory in HOL4

作　　者：刘振科[1] 施智平[1,2] 关永[1] 金声震[1] 张杰[3] 叶世伟[4] 李晓娟[1] 

机构地区：[1]电子系统可靠性技术北京市重点实验室首都师范大学信息工程学院,北京100048 [2]计算机体系结构国家重点实验室中国科学院计算技术研究所,北京100190 [3]北京化工大学信息科学与技术学院,北京100029 [4]中国科学院研究生院信息科学与工程学院,北京100049

出　　处：《小型微型计算机系统》2013年第3期654-658,共5页Journal of Chinese Computer Systems

基　　金：国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035)资助;北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028036)资助;北京市优秀人才培养资助项目;计算机体系结构国家重点实验室开放课题

摘　　要：定理证明是重要的形式化验证方法之一,其将系统建模为逻辑公式,依托定理证明器进行推理从而完成验证.定理证明器中包含的定理库越多,其建模和推理能力越强.控制理论中经常用函数向量描述状态空间,形式化函数矩阵理论对控制系统的形式化分析有重要意义.本文在高阶逻辑定理证明器Higher-Order Logic 4中形式化函数向量和函数矩阵,包括形式化定义数据类型、运算及形式化验证运算性.本文同时给出了函数矩阵求导的形式化定义,证明了矩阵微分法中函数矩阵(或函数向量)相对于数量变量的微分法的常用定理,并给出了对二次型函数求导的形式化证明.本文工作已整理成定理库.Theorem proving is one of the most important methods of formal verification,it model the system for logic formula,reasoning and complete verification relying on theorem prover.The more the theorem prover contains theorem library,the stronger its reasoning ability.Function matrices are widely used in the control theory to describe state space.Formalizing the function matrix theory is significant for the formal analysis of control systems.Based on the higher order logical theorem prover Higher-Order Logic 4,this paper formalizes the function vector and function matrix theory,including data types,operations and their properties.The paper also presents the formal definition of the function matrix derivative,proves the commonly used theorems of the function matrix(or function vector) differential on quantity variables and presents the formal proof of quadratic function derivative.The formalization is implemented as a library in the Higher-Order Logic 4 system.

关 键 词：函数矩阵 形式化验证 矩阵微分法 定理证明 HIGHER-ORDER Logic4 

分 类 号：TN319[电子电信—物理电子学]