实数二项式系数在HOL4中的形式化

计算机科学 ›› 2014, Vol. 41 ›› Issue (2): 15-18.

实数二项式系数在HOL4中的形式化

师丽坤,赵春娜,关永,施智平,李晓娟,叶世伟

首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048;首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048;中国科学院研究生院信息科学与工程学院北京100049

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受国际科技合作计划(2010DFB10930,1DFG13000),国家自然科学基金项目(60873006,61070049,4,61104035,5,61201378),北京市自然科学基金、北京市优秀人才项目(4122017,KZ201210028036,KM201010028021,2012D005016000011)资助

Formalization of Real Binomial Coefficient in HOL4

SHI Li-kun,ZHAO Chun-na,GUAN Yong,SHI Zhi-ping,LI Xiao-juan and YE Shi-wei

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： 定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。

关键词: 实数二项式系数,高阶逻辑,定理证明,HOL4,分数阶微积分中图法分类号TP319文献标识码A

Abstract: The theorem proving is a formal method and plays an important role in the verification of safety-critical system．The fractional calculus is the basis of the complex system’s analysis．The real binomial coefficient is an important part of the fractional calculus GL definition．Currently,there is not the formalization of real binomial coefficient in higher-order-logic theorem library．This paper presented the formalization of the real binomial coefficients．The factorial power was firstly formalized in HOL4．And the real binomial coefficient was formalized using the formalization of factorial power．The paper also presented the formal verification of the fractional calculus．At the same time it illustrateed the practical effectiveness and utilization of our approach.

Key words: Real binomial coefficient,High order logic,Theorem proof,HOL4,Fractional calculus

师丽坤,赵春娜,关永,施智平,李晓娟,叶世伟. 实数二项式系数在HOL4中的形式化[J]. 计算机科学, 2014, 41(2): 15-18. https://doi.org/

SHI Li-kun,ZHAO Chun-na,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. https://doi.org/

参考文献

[1] 王戟,李宣东.形式化方法与工具专刊前言[J].软件学报,2011,2(6):1121-1122
[2] 韩俊刚,杜慧敏．数字硬件的形式化验证[M]．北京:北京大学出版社,2001
[3] 万哲先．二项式系数和Gauss系数[J]．数学通报,1994,0:1-6
[4] Podlubng I．Fractional Differential Equations[M]．Technical University of Kosice,Slovak Repubic,1999
[5] Harrison J．Theorem Proving with the Real Numbers[M]．Springer-Verlag,1998
[6] Graham,Knuth R L,Patashnik D E,et al.Concrete Mathema-tics:A Foundation for Computer Science[M]．1994
[7] 万哲先．介绍广义二项式系数[J]．数学通报,2000(1):34-37
[8] 赵春娜,李英顺,陆涛．分数阶系统分析与设计[M]．北京:国防工业出版社,2011
[9] Mhamdi T,Hasan O,Tahar S．On the Formalization of the Lebesgue Integration Theory in HOL[C]∥Interactive Theorem Proving,volume 6172of Lecture Notes in Computer Science．Springer,2010:387-402
[10] 谷伟卿,施智平,关永,等．Gauge积分在HOL4中的形式化[J]．计算机科学,2013,0(2):191-194
[11] 王东风,王晓燕,韩璞．锅炉-汽轮机系统的分数阶控制器设计[J]．中国电机工程学报,2010(5):113-119
[12] 黄果,许黎,蒲亦非．分数阶微积分在图像处理中的研究综述[J]．计算机应用研究,2012,29(2):414-420
[13] 殷德顺,任俊娟,和成亮,等．基于分数阶微积分理论的软土应力-应变关系[J]．岩石力学与工程学报,2009,8(A01):2973-2979
[14] 孙建新．阶乘幂多项式及其基本恒等式[J]．绍兴文理学院学报,2004,4(7):34-37
[15] Maione G,Lino P．New Tuning Rules for Fractional PIα Controllers[J]．Nonlinear Dynamics,2007,49(1/2):251-257
[16] 蒲亦菲．分数阶微积分在现在信号分析与处理中应用的研究[D]．成都:四川大学,2006
[17] Chang T-S,Singh M P．Seismic analysis of structures with afractional derivative model of viscoelastic dampers[J]．Earthquake Engineering and Engineering Vibration,2002,1(2):251-260
[18] Mandelbrot B B．The fractal geometry of nature[M]．San Francisco:Freeman,1982

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed