| 分数阶微积分定义的一致性在HOL4中的验证 |
| |
| 引用本文： | 李姗姗,赵春娜,关永,施智平,王瑞,李晓娟,叶世伟. 分数阶微积分定义的一致性在HOL4中的验证[J]. 计算机科学, 2016, 43(3): 23-26 |
| |
| 作者姓名： | 李姗姗 赵春娜 关永 施智平 王瑞 李晓娟 叶世伟 |
| |
| 作者单位： | 首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048,中国科学院大学信息科学与工程学院 北京100049 |
| |
| 基金项目： | 本文受国际科技合作计划项目(2010DFB10930,2011DFG13000),国家自然科学基金项目(60873006,61070049,61170304,61104035,61174145,61201378),北京市自然科学基金项目,北京市优秀人才项目(4122017,KZ201210028036,KM201010028021,2012D005016000011)资助 |
| |
| 摘 要： | 分数阶微积分有3种常用的定义:Grunwald-Letnikov定义、Riemann-Liouville定义以及Caputo定义,3种定义之间存在着一定的联系,在一定条件下,它们可以相互转换。首先在高阶逻辑定理证明器HOL4中使用实数、积分、极限、超越函数等定理建立了基于Caputo定义的分数阶微积分形式化模型；然后验证了该定义与Grunwald-Letni-kov定义、Riemann-Liouville定义之间的关系,实现了这3种常用定义在HOL4中的转换,在一定程度上使这3种定义达到了统一,完善了高阶逻辑定理库。
|
| 关 键 词： | 分数阶微积分 定理证明 Caputo定义 一致性 |
| 收稿时间： | 2015-01-31 |
| 修稿时间： | 2015-04-06 |
Formalization of Consistency of Fractional Calculus in HOL4 |
| |
| LI Shan-shan,ZHAO Chun-n,GUAN Yong,SHI Zhi-ping,WANG Rui,LI Xiao-juan and YE Shi-wei. Formalization of Consistency of Fractional Calculus in HOL4[J]. Computer Science, 2016, 43(3): 23-26 |
| |
| Authors: | LI Shan-shan ZHAO Chun-n GUAN Yong SHI Zhi-ping WANG Rui LI Xiao-juan YE Shi-wei |
| |
| Affiliation: | Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,College of Information Engineering Capital Normal University,Beijing 100048,China and College of Information Science and Engineering,University of Chinese Academy of Sciences,Beijing 100049,China |
| |
| 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. |
| |
| Keywords: | Fractional calculus Theorem proving Caputo definition Consistency |
| 本文献已被 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
