Gauge积分在HOL4中的形式化

摘要：

积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等.Gauge积分是黎曼积分在闭区间上的推广,应用更加方便.将Gauge积分的运算性质在HOLA (Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则,并根据相关性质对反相积分器进行了验证.

关键词：形式化验证、定理证明、Gauge积分、HOL4、积分器

所属期刊栏目：40

分类号：TP301.2(计算技术、计算机技术)

资助基金：国际科技合作计划2010DFB10930,2011DFG13000;国家自然科学基金项目61070049,61170304,61104035;北京市自然科学基金

在线出版日期：2013-03-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：191-194,228