%0 Journal Article
%T gauge积分在hol4中的形式化
%A 谷伟卿
%A 施智平
%A 关永
%A 张杰
%A 赵春娜
%A 叶世伟？
%J 计算机科学
%D 2013
%X 积分是许多数学理论的基础，如实数分析、信号与系统中微分方程的求解等等。gauge积分是黎曼积分在闭区间上的推广，应用更加方便。将gauge积分的运算性质在hol4(higher-orderlogic4)中形式化，包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则，并根据相关性质对反相积分器进行了验证。
%K 形式化验证
%K 定理证明
%K gauge积分
%K hol4
%K 积分器
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=130242&flag=1