摘要
积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则,并根据相关性质对反相积分器进行了验证。
Integral is one of the most important foundations in many subjects, such as real analysis, the differential equa tions in signals and systems and so on. Gauge integral is a generalization of the Riemann integral in which some situa- tions are more useful than the Lebesgue integral. This paper formalized the operational properties which contain the fin- earity, ordering properties, integration by parts, the special functions and limit theorem, eauehy-type (HOIA), and then used them to verify an inverting integral split theorem,integrability on a subinterval, integrability of integrability criterion of gauge integral in higher-order-logic 4 integrator.
出处
《计算机科学》
CSCD
北大核心
2013年第2期191-194,228,共5页
Computer Science
基金
国际科技合作计划(2010DFB10930
2011DFG13000)
国家自然科学基金项目(61070049
61170304
61104035)
北京市自然科学基金项目资助