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

Formalization of Consistency of Fractional Calculus in HOL4

分数阶微积分有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.