计算机科学 ›› 2016, Vol. 43 ›› Issue (11): 24-29.doi: 10.11896/j.issn.1002-137X.2016.11.005
杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰
YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie
摘要: 函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。
[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! |
|