计算机科学 ›› 2013, Vol. 40 ›› Issue (2): 191-194.228.
• 软件与数据库技术 • 上一篇 下一篇
谷伟卿,施智平,关永,张杰,赵春娜,叶世伟
出版日期:
发布日期:
Online:
Published:
摘要: 积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭 区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4 (Higher-Order Logic 4)中形式化,包括积分的线 性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯 西可积准则,并根据相关性质对反相积分器进行了验证。
关键词: 形式化验证,定理证明,Gauge积分,HOL4,积分器
Abstract: Integral is one of the most important foundations in many subjects, such as real analysis, the differential equa- lions in signals and systems and so on. Gauge integral is a generalization of the Riemann integral in which some situa- lions are more useful than the Lebesgue integral. This paper formalized the operational properties which contain the fin- rarity, ordering properties, integration by parts, the integral split theorem, integrability on a subinterval, integrability of special functions and limit theorem, cauchy-type integrability criterion of gauge integral in higher-order-logic 4 (HOL4) , and then used them to verify an inverting integrator.
Key words: Formal verification, Thcorcm proving, Gauge integral, HOL4, Integrator
谷伟卿,施智平,关永,张杰,赵春娜,叶世伟. Gauge积分在HOL4中的形式化[J]. 计算机科学, 2013, 40(2): 191-194.228. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2013/V40/I2/191
Cited