| 实数二项式系数在HOL4中的形式化 |
| |
| 引用本文： | 师丽坤,赵春娜,关永,施智平,李晓娟,叶世伟.实数二项式系数在HOL4中的形式化[J].计算机科学,2014,41(2):15-18. |
| |
| 作者姓名： | 师丽坤 赵春娜 关永 施智平 李晓娟 叶世伟 |
| |
| 作者单位： | 首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 北京100048;中国科学院研究生院信息科学与工程学院 北京100049 |
| |
| 基金项目： | 本文受国际科技合作计划(2010DFB10930,1DFG13000),国家自然科学基金项目(60873006,61070049,4,61104035,5,61201378),北京市自然科学基金、北京市优秀人才项目(4122017,KZ201210028036,KM201010028021,2012D005016000011)资助 |
| |
| 摘 要： | 定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。
|
| 关 键 词： | 实数二项式系数 高阶逻辑 定理证明 HOL 分数阶微积分 |
| 收稿时间： | 2013/4/21 0:00:00 |
| 修稿时间： | 2013/6/21 0:00:00 |
Formalization of Real Binomial Coefficient in HOL4 |
| |
| SHI Li-kun,ZHAO Chun-n,GUAN Yong,SHI Zhi-ping,LI Xiao-juan and YE Shi-wei.Formalization of Real Binomial Coefficient in HOL4[J].Computer Science,2014,41(2):15-18. |
| |
| Authors: | SHI Li-kun ZHAO Chun-n GUAN Yong SHI Zhi-ping LI Xiao-juan and YE Shi-wei |
| |
| Affiliation: | Beijing Engineering Research Center of High Reliable Embedded System,College of Information Engineering, Capital Normal University,Beijing 100048,China;Beijing Engineering Research Center of High Reliable Embedded System,College of Information Engineering, Capital Normal University,Beijing 100048,China;Beijing Engineering Research Center of High Reliable Embedded System,College of Information Engineering, Capital Normal University,Beijing 100048,China;Beijing Engineering Research Center of High Reliable Embedded System,College of Information Engineering, Capital Normal University,Beijing 100048,China;Beijing Engineering Research Center of High Reliable Embedded System,College of Information Engineering, Capital Normal University,Beijing 100048,China;College of Information Science and Engineering,Graduate University,Chinese Academy of Sciences,Beijing 100049,China |
| |
| Abstract: | |
| |
| Keywords: | Real binomial coefficient High order logic Theorem proof HOL4 Fractional calculus |
| 本文献已被 CNKI 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
