计算机科学 ›› 2016, Vol. 43 ›› Issue (11): 24-29.doi: 10.11896/j.issn.1002-137X.2016.11.005

• 目次 • 上一篇    下一篇

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

杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰   

  1. 首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室 北京100048,首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室 北京100048,首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室 北京100048,首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室 北京100048,首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室 北京100048,北京化工大学信息科学与技术学院 北京100029
  • 出版日期:2018-12-01 发布日期:2018-12-01
  • 基金资助:
    本文受国际科技合作计划(2011DFG13000),国家自然科学基金项目(61170304,8,61572331),北京市科委项目(Z141100002014001),北京市教委科研基地建设项目(TJSHG201310028014),北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助

Higher-order Logic Formalization of Function Matrix and its Calculus

YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie   

  • Online:2018-12-01 Published:2018-12-01

摘要: 函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。

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

Abstract: 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.

Key words: Function matrix,Calculus,Formal verification,Higher-order logic theorem proving

[1] 胡寿松.自动控制原理[M].北京:科学出版社,2008
[2] Huang Ke-jin,Qian Ji-xin,Sun You-xian,et al.A kind of theoretical derivation method of rectifying column transfer function matrix[J].Journal of Zhejiang University,1994,28(3):253-261(in Chinese) 黄克谨,钱积新,孙优贤,等.一种精馏塔传递函数矩阵的理论推导方法[J].浙江大学学报,1994,8(3):253-261
[3] Shen Yu-ling.Multivariable control system analysis and design based on the equivalent transfer function[D].Shanghai:Shanghai Jiaotong University,2012(in Chinese) 沈玉玲.基于等价传递函数的多变量控制系统分析与设计[D].上海:上海交通大学,2012
[4] Vladimir N,Sidorova Sergey M,et al.Discrete-analytic solutionof unsteady-state heat conduction transfer problem based on a theory of matrix function [J].Procedia Engineering,2015,111:726-733
[5] Hu Liang,Gu Ming,Li Li.Proper orthogonal decomposition of the wind field based on the coherence function matrix [J].Journal of Vibration Engineering,2010,23(1):64-68(in Chinese) 胡亮,顾明,李黎.基于相干函数矩阵的风场本征正交分解[J].振动工程学报,2010,3(1):64-68
[6] Babolian E,Fattahzadeh F.Numerical solution of differential equations by using Chebyshev wavelet operational matrix of integration[J].Applied Mathematics & Computation,2007,8:417-426
[7] Taubig H,Frese U,Hertzberg C,et al.Guaranteeing functional safety:design for provability and computer-aided verification[J].Autonomous Robots,2012,32(3):303-331
[8] Hasan O,Tahar S,et al.Formal Reliability Analysis Using Theo-rem Proving[J].IEEE Transactions on Computers ,2010,9(5):579-592
[9] Gordon M,Melham T.Introduction to HOL:A Theorem Pro-ving Environment for Higher-Order Logic[M].Cambridge:Cambridge Univ.Press,1993
[10] Shi Z,Zhang Y,Liu Z,et al.Formalization of Matrix Theory in HOL4[J].Advances in Mechanical Engineering,2014,6:1-16
[11] Shi Zhi-ping,Liu Zhen-ke,Guan Yong,et al.Formalization ofFunction Matrix Theory in HOL[J].Advances in Mechanic Engineering,2014,3:1-16
[12] 程云鹏,张凯院,徐仲.矩阵论(第三版)[M].西安:西北工业大学出版社,2006
[13] Gu Wei-qing,Shi Zhi-ping,Guan Yong,et al.Formalization of Gauge Integration Theory in HOL4[J].Computer Science,2013,0(2):191-194(in Chinese) 谷伟卿,施智平,关永,等.Gauge积分在HOL4中的形式化[J].计算机科学,2013,0(2):191-194

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!