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

• 作者: 关永 叶世伟 施智平 李姗姗 李晓娟 王瑞 赵春娜
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 分数阶微积分 定理证明 Caputo定义 一致性
• 年，卷（期）: 2016,（3）
• 页码范围: 23-26,53
• 页数: 5页
• 分类号: TP301.2
• 字数: 7365字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.3.004

摘要

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