函数矩阵及其微积分的高阶逻辑形式化  

Higher-order Logic Formalization of Function Matrix and its Calculus

作　　者：杨秀梅[1] 关永[1] 施智平[1] 吴爱轩 张倩颖[1] 张杰[2] 

机构地区：[1]首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室,北京100048 [2]北京化工大学信息科学与技术学院,北京100029

出　　处：《计算机科学》2016年第11期24-29,共6页Computer Science

基　　金：国际科技合作计划(2011DFG13000);国家自然科学基金项目(61170304;61472468;61572331);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助

摘　　要：函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。Function matrix is widely employed in the modeling and analysis of dynamic system.Paper-pencil calculations,numerical calculations and symbolic algebra methods,which are used in traditional analysis of function matrix,cannot guarantee to provide accurate or correct results.Higher-order logic theorem proving,as a kind of highly reliable formal verification method,can overcome the above shortcomings.This paper formalized the related theories of function vector and function matrix in the higher-order logic theorem prover HOL4.Formal contents include the formal definitions and proving of function vector and function matrix,and their properties of continuity,differential and integral.The formal verification of the differential equation of rotation matrix in the robotic kinematics was given to illustrate the application of the formalization.

关 键 词：函数矩阵 微积分性质 形式化验证 高阶逻辑定理证明 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]