Computer Science ›› 2016, Vol. 43 ›› Issue (3): 23-26.doi: 10.11896/j.issn.1002-137X.2016.03.004

Previous Articles     Next Articles

Formalization of Consistency of Fractional Calculus in HOL4

LI Shan-shan, ZHAO Chun-na, GUAN Yong, SHI Zhi-ping, WANG Rui, LI Xiao-juan and YE Shi-wei   

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

Abstract: Fractional calculus has three commonly used definitions,including Grunwald-Letnikov,Riemann-Liouville and Caputo definition.There are connections among these three kinds of definitions.They are interchangeable under certain conditions.This paper established a formal model of fractional calculus based on Caputo definition in the higher-order logic proof tool HOL4 using real,integral,limitation and transcendental functions.In order to achieve the conversion of these three definitions in HOL4,we verified the relationships among Caputo,Grunwald-Letnikov and Riemann-Liouville definition.This work will make these three definitions unite in a certain extent,and will also perfect the theo-rem library of higher-order logic.

Key words: Fractional calculus,Theorem proving,Caputo definition,Consistency

[1] Dalir M.Applications of Fractional Calculus[J].Applied Mathematical Sciences,2010,4(21):1021-1032
[2] Tomovsk ,Garra R.Analytic Solutions of Factional Integro-Differential Equations of Volterra Type with Variable Coefficients[J].Fractional Calculus & Applied Analysis,2014,7(1):38-60
[3] Siddique U,Hasan O.Formal Analysis of Fractional Order Systems in HOL[C]∥2011 IEEE Formal Methods in Computer-Aided Design.2011:163-170
[4] Shi Li-kun.Formal Analysis of Fractional Systems Based onGrunwald-Letnikov Definition using High Order Logic[D].Beijing:Capital Normal University,2014(in Chinese) 师丽坤.基于Grunwald-Letnikov定义的分数阶系统高阶逻辑形式化分析[D].北京:首都师范大学,2014
[5] Zhao Chun-na,Li Ying-shun,Lu Tao.Analysis and Design ofFractional Systems[M].Beijing:National Defend Industry Press,2010:13-20(in Chinese) 赵春娜,李英顺,陆涛.分数阶系统分析与设计[M].北京:国防工业出版社,2010:13-20
[6] Harrison J.Theorem Proving with the Real Numbers[M].Springer-Verlag,1998
[7] Gu Wei-qing,Shi Zhi-ping,Guan Yong,et al.Formalization ofGauge Integration Theory in HOL4[J].Computer Science,2013,40(2):191-194(in Chinese) 谷伟卿,施智平,关永,等.Gauge积分在HOL4中的形式化[J].计算机科学,2013,40(2):191-194
[8] Zhao Gang,Zhao Chun-na,Guan Yong,et al.Formalization ofLaplace Transform Calculus in HOL4[J].Journal of Chinese Computer System,2014,35(9):2178-2181(in Chinese) 赵刚,赵春娜,关永,等.拉普拉斯变换微积分性质在HOL4中的形式化[J].小型微型计算机系统,2014,5(9):2178-2181
[9] Shi Li-kun,Zhao Chun-na,Guan Yong,et al.Formalization ofReal Binomial Coefficient in HOL4[J].Computer Science,2014,41(2):15-18(in Chinese) 师丽坤,赵春娜,关永,等.实数二项式系数在HOL4中的形式化[J].计算机科学,2014,41(2):15-18
[10] Zhou Ji-liu,Pu Yi-fei,Liao Ke.Fractional Calculus Principle and its Application in the Analysis and Processing of Modern Signal[M].Beijing:Science Press,2006:14-16(in Chinese) 周激流,蒲亦菲,廖科.分数阶微积分原理及其在现代信号分析与处理中的应用[M].北京:科学出版社,2006:14-16
[11] Wang Chun-yang.Study on Fractional Order PIλDμ Controller Parameter Tuning methods and Design[D].Jilin:Jilin University,2013(in Chinese) 王春阳.分数阶PID控制器参数整定方法与设计研究[D].吉林:吉林大学,2013
[12] Wang Ji-feng.Analysis of Control Performance for FractionalOrder Systems[M].Beijing:Publishing House of Electronics Industry,2010:13-14(in Chinese) 汪纪锋.分数阶系统控制性能分析[M].北京:电子工业出版社,2010:13-14
[13] Chen Wen,Sun Hong-guang,Li Xi-cheng.Fractional Derivative Model of Mechanical and Engineering Problems [M].Beijing:Science Press,2010:18-19(in Chinese) 陈文,孙洪广,李西成.力学与工程问题的分数阶导数建模[M].北京:科学出版社,2010:18-19

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 .