论文部分内容阅读
在高阶逻辑定理证明器中研究了函数无穷远处极限的形式化建模和验证,包括函数无穷远处极限定义的形式化模型,函数极限相关性质的建模与验证,有唯一性、保不等式性、绝对值函数在无穷远处的极限、极限等价性、常函数极限等.函数无穷远处极限的高阶逻辑定义是利用拓扑极限方式定义的,并在实数域内利用集合关系等验证定理.根据集合有序关系定理验证了唯一性.利用差值和绝对值的高阶逻辑性质验证极限为零的属性.变量与常数之和与积的极限高阶逻辑定理也通过已验证定理和高阶逻辑策略验证了.建立了函数极限四则运算的高阶逻辑模型,并验证了函数极