• 目次 •

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

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

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.

 [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