文献类型：期刊文章

作　　者：谷伟卿[1] 施智平[1] 关永[1] 张杰[2] 赵春娜[1] 叶世伟[3]

机构地区：[1]首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心 [2]北京化工大学信息科学与技术学院 [3]中国科学院研究生院信息科学与工程学院

出　　处：《计算机科学》

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

年　　份：2013

卷　　号：40

期　　号：2

起止页码：191-194

语　　种：中文

收录情况：BDHX、BDHX2011、CSA、CSCD、CSCD2013_2014、IC、JST、RCCSE、UPD、ZGKJHX、核心刊

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

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

分 类 号：TP301.2]