Computer Science ›› 2016, Vol. 43 ›› Issue (11): 24-29.doi: 10.11896/j.issn.1002-137X.2016.11.005

Previous Articles     Next Articles

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.

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!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .