分数阶微积分定义的一致性在HOL4中的验证  

Formalization of Consistency of Fractional Calculus in HOL4

作　　者：李姗姗[1] 赵春娜[1] 关永[1] 施智平[1] 王瑞[1] 李晓娟[1] 叶世伟[2] 

机构地区：[1]首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心,北京100048 [2]中国科学院大学信息科学与工程学院,北京100049

出　　处：《计算机科学》2016年第3期23-26,53,共5页Computer Science

基　　金：国际科技合作计划项目(2010DFB10930;2011DFG13000);国家自然科学基金项目(60873006;61070049;61170304;61104035;61174145;61201378);北京市自然科学基金项目;北京市优秀人才项目(4122017;KZ201210028036;KM201010028021;2012D005016000011)资助

摘　　要：分数阶微积分有3种常用的定义:Grunwald-Letnikov定义、Riemann-Liouville定义以及Caputo定义,3种定义之间存在着一定的联系,在一定条件下,它们可以相互转换。首先在高阶逻辑定理证明器HOL4中使用实数、积分、极限、超越函数等定理建立了基于Caputo定义的分数阶微积分形式化模型;然后验证了该定义与Grunwald-Letnikov定义、Riemann-Liouville定义之间的关系,实现了这3种常用定义在HOL4中的转换,在一定程度上使这3种定义达到了统一,完善了高阶逻辑定理库。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.

关 键 词：分数阶微积分 定理证明 Caputo定义 一致性 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]