Gauge积分在HOL4中的形式化

• 作者: 关永 叶世伟 张杰 施智平 谷伟卿 赵春娜
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 形式化验证 定理证明 Gauge积分 HOL4 积分器
• 年，卷（期）: 2013,（2）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 191-194,228
• 页数: 5页
• 分类号: TP301.2
• 字数: 3804字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	关永	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	95	1336	17.0	33.0
3	叶世伟	中国科学院研究生院信息科学与工程学院	30	250	8.0	15.0
4	施智平	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	24	145	8.0	11.0
5	赵春娜	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	9	88	4.0	9.0
6	谷伟卿	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	1	7	1.0	1.0