函数极限的高阶逻辑形式化建模与验证

• 作者: 赵刚 赵春娜
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 函数极限 高阶逻辑 形式化验证 定理证明 卷积
• 年，卷（期）: 2020,（11）
• 页码范围: 2119-2133
• 页数: 15页
• 分类号: TP18
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2020.02119

摘要

在高阶逻辑定理证明器中研究了函数无穷远处极限的形式化建模和验证,包括函数无穷远处极限定义的形式化模型,函数极限相关性质的建模与验证,有唯一性、保不等式性、绝对值函数在无穷远处的极限、极限等价性、常函数极限等.函数无穷远处极限的高阶逻辑定义是利用拓扑极限方式定义的,并在实数域内利用集合关系等验证定理.根据集合有序关系定理验证了唯一性.利用差值和绝对值的高阶逻辑性质验证极限为零的属性.变量与常数之和与积的极限高阶逻辑定理也通过已验证定理和高阶逻辑策略验证了.建立了函数极限四则运算的高阶逻辑模型,并验证了函数极限加法、函数极限减法、函数极限乘法、函数极限与常数乘法、函数极限除法的高阶逻辑定理.也建立了函数积分极限的高阶逻辑形式化模型,验证了函数积分极限上限绝对值定理、函数积分极限上限可加定理、函数积分极限上限可乘定理.在此基础上,建立了拉普拉斯变换卷积定理的高阶逻辑形式化建模与验证.最后,对电阻电感电路中的电流进行了高阶逻辑形式化建模与验证,建立了单位阶跃信号和电路中电流的高阶逻辑形式化定义,并验证了其正确性.该实例验证表明了函数极限和相关性质的高阶逻辑形式化模型的正确性,为后续控制系统的形式化分析奠定了良好的基础.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵春娜		3	0	0.0	0.0
2	赵刚		3	29	1.0	3.0