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

【Abstract】 Integral is one of the most important foundations in many subjects,such as real analysis,the differential equations in signals and systems and so on.Gauge integral is a generalization of the Riemann integral in which some situations are more useful than the Lebesgue integral.This paper formalized the operational properties which contain the linearity,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.更多还原