引言人工智能一直是科技界的一个努力方向， 能够与人类互动的机器人更是人们研究的热点之一．２ ０ １ ５ 年７ 月， 德国大众工厂发生“ 机器人杀人”事件．提高机器人的可靠性和安全性是机器人应用的至关重要的问题． 机器人系统的可靠性主要依赖于其控制系统． 形式化方法是基于数学方法描述目标系统属性的一种技术， 它提供了更完备的验证结果， 为交互式机器人的安全验证提供了坚实的基础． 髙阶逻辑定理证明方法是形式化方法中一种严谨的验证方法． 在高阶逻辑定理证明方法中， 机器人核心控制系统的验证需要很多定理库的支持， 其中拉普拉斯变换的形式化是一个重要的内容． 拉普拉斯变换的形式化是以函数极限和相关性质的高阶逻辑形式化为基础的．函数极限是数学中的基本概念之一， 也是拉普拉斯变换等的理论基础， 本文在高阶逻辑定理证明器中研究了函数正无穷大时极限及相关性质的形式化建模和验证， 为控制系统的高阶逻辑验证提供基础理论． 第２ 节介绍高阶逻辑定理证明器； 第３ 节建立函数正无穷大时极限的高阶逻辑模型； 第４ 节对函数极限的基本性质、四则运算和函数积分极限的一些性质进行形式化建模和验证； 第５ 节对拉普拉斯变换卷积定理建立高阶逻辑形式化模型； 第６ 节应用本文的内容对电阻－ 电感电路（ 简称ＲＬ 电路）中的电流进行高阶逻辑形式化建模与验证．２ 高阶逻辑定理证明器定理证明是形式化方法的一种， 它是一种用数学逻辑公式来表达系统及其属性的技术， 通过对现实中的物理模型提取属性性质转换为数学模型， 再由数学模型转换为逻辑模型， 并在相关定理证明器中进行描述， 从而得到一个形式化系统， 找到某属性的一个证明过程． 定理证明是一种交互式分析技术．它的分析原理是为系统的需求规范和设计实现建立逻辑模型， 然后通过形式化定理验证两者的关系． 如果该定理通过证明是正确的， 则说明实现和需求之间是等价的或是蕴含的． 定理证明克服了等价性验证需要建立标准模型和模型检测处理复杂系统会产生空间爆炸的约束的问题． 由于定理证明器可以表达所有可以逻辑化的东西， 它已用于多个领域的可靠性分析， 如应用高阶逻辑来验证操作系统的安全需求［ Ｓ赵春娜等： 函数极限的１ １ 期 高阶逻辑形式化建模与验证 ２ １ ２ １文献［２］ 用高阶逻辑表达线性时态逻辑和区间时态逻辑， 并以实例说明它在硬件设计验证中的应用；应用定理证明也可以来验证多机器人路径规划的安全性文献［４］ 在高阶逻辑证明工具Ｈ Ｏ Ｌ－ Ｌ ｉ ｇｈ ｔ中建立了几何代数系统的形式化模型等等． 定理证明虽然可以表达所有可逻辑化的系统， 但是证明定理时需要人工引导， 于是要求定理证明器的使用者熟悉逻辑推理并且拥有一定的推理经验， 这是定理证明难以大众化的原因． 目前， 定理证明主要应用于一些系统关键性质的分析， 在特殊领域里定理证明发挥了巨大优势． 定理证明技术逐渐成为形式化验证技术的重点研究方向， 在研究和应用上都拥有巨大的发展潜力？定理证明本质是， 基于系统的公理及推导规则来为定理寻找证明［５］． 当演绎推理和数学定理的手工推导证明， 变化成为符号演算的过程技术， 并且可以在计算机上自动进行时， 定理证明就成为当今软件工程领域中一种非常重要的形式验证技术［ ６］， 即定理证明系统． 在运用定理证明的方法进行系统设计验证时， 辅助手工推导的计算机程序被称为机械定理证明器， 它和自动定理证明器组成了自动化程度不同的定理证明器． 现在， 具有各种特点的定理证明系统已成为教育、学术及工业界的有力工具． 这些定理证明系统拥有各种不同的特性， 主要系统有Ａ ＣＬ２ 、Ｃ ｏｑ 、Ｌｅｇ ｏ 、Ｉｓ ａ ｂｅ ｌ ｌ ｅ 、Ｈ Ｏ Ｌ和 Ｐ ＶＳ等？Ａ ＣＬ２是由早期用于软件验证的定理证明器Ｂｏ ｙｅ ｒ－Ｍ ｏｏｒｅ发展来的， Ａ ＣＬ２ 从设计上支持基于归纳逻辑理论的自动推理， 可应用于软件或硬件系统的验证．ＡＣＬ２ 定理证明器的核心是基于项重写系统． Ｃｏｑ支持数学断言的表达式， 机械化地对这些断言执行检查， 辅助寻找正式证明， 并从其形式化描述的构造性证明中提取出可验证的程序． Ｃｏｑ 基于归纳构造演算， 是构造演算的一种衍生理论．Ｈ Ｏ Ｌ （ Ｈｉ ｇ ｈｅ ｒ－ 〇ｒｄｅ ｒ Ｌｏｇ ｉ ｃ ） 是定理证明中的高阶逻辑定理证明器， 由Ｇ ｏｒｄ ｏｎ 于２ ０ 世纪８ ０ 年代中期在英国剑桥大学创建的高阶逻辑系统［ ７ ８ ］， 其主要特点是通过Ｍ Ｌ （ Ｍ ｅ ｔａ Ｌ ａ ｎ ｇｕ ａｇ ｅ 是一个通用的函数式编程语言） 语言实现高度的可编程性． 本文采用的版本是ＨＯ Ｌ４ ， 该工具是利用缜密的数学逻辑来实现工业验证的精确性． Ｍ Ｌ 是一种强类型函数程序设计语言， 是比较经典的函数式语言， 其所有对象的类型都必须在编译的时候静态分析决定．ＭＬ 提供的类型有单元（ ｕ ｎｉ ｔ ） 、布尔型（ ｂｏ ｏｌ ） 、整型（ ｉ ｎ ｔ ） 、字符串型（ ｓ ｔ ｒ ｉ ｎｇ ） 、实数（ ｒ ｅ ａ ｌ ） 、元组（ ｔ ｕ ｐ ｌ ｅ ） 、记录（ ｒ ｅ ｃｏ ｒｄ） 和列表（ ｌ ｉ ｓ ｔ ） ． ＭＬ 还支持模式匹配、意外处理、类型引用、多态性以及递归数据结构． 它拥有自然的语法和较少的基本概念， 其理论基础是Ａ演算， 语言实现严谨、高效且易于理解， 用户可以容易写出清晰可靠的程序． 大多数著名的推理系统都是用Ｍ Ｌ 语言编写的． Ｍ Ｌ 语言作为一种函数式编程语言， 减少了指针的使用， 并提供了灵活的表达方式， 有助于管理复杂的对象． ＭＬ 编译器循环地进行“输入－求值－输出”， 用户标准的操作方式是一条一条地输人Ｍ Ｌ 表达式或者声明， 让Ｍ Ｌ 编译器去处理． Ｍ Ｌ 编译器处理的过程包括类型检査、编译、执行． Ｍ Ｌ 家族有好几种语言， 主要的两种语言是Ｃａ ｍ ｌ 和标准ＭＬ ， 标准Ｍ Ｌ 语言被简称为ＳＭＬ ， 或者直接称为ＭＬ ．ＭＬ 语言结合了函数式编程语言和命令式编程语言的特点， 这是它得以广泛应用的重要原因．在定理证明器Ｈ Ｏ Ｌ４ 中进行形式化证明时， 如要使用定理库里相关的定义和定理， 需要先用ｌ ｏａ ｄ和ｏ ｐｅ ｎ 语句加载并打开相应的定理库． ＨＯ Ｌ ４ 有非常丰富的定理库， 并且由于其庞大的用户基础， 定理库会越来越丰富． 随着Ｈ Ｏ Ｌ４ 定理库越来越完善， 其应用也越来越广泛． 加拿大Ｃｏｎ ｃｏ ｒｄ ｉａ 大学的Ｓ ｉ ｄｄ ｉｑ ｕ ｅ 等人在高阶逻辑定理证明器Ｈ Ｏ Ｌ 中验证了分数阶微积分ＲＬ 定义［９］ 和Ｇ ａ ｍｍ ａ 函数［ １ ＂］； Ｌｉ ｕ等人在髙阶逻辑定理证明器ＨＯ Ｌ 中验证了马尔科夫链［１ １ ］， 为系统的状态验证提供基础． Ｋ ｕｍａ ｒ 等人利用Ｈ Ｏ Ｌ 分析了Ｄ Ｎ Ａ 中的纳米生物规模的化学信息处理动态Ｄ ２］， 开发利用全息理解分子尺度生物化学计算行为的新形式． Ａ ｈ ｍｅ ｄ 等人在ＨＯＬ 中对可靠性框图进行了形式化验证［１ ３］， 对串并联、平行、嵌套等建立了形式化模型， 并验证了云计算中心的一个通用的虚拟数据的可靠性． 巴基斯坦的Ｓ ａ ｒ ｄａ ｒ等人对于分布式动态热管理系统， 应用高阶逻辑方法验证系统的性能和时间属性［ Ｍ ］， 包括热性能、温度范围、达到热稳定性时间等． 文献［ １ ５］ 在ＨＯ Ｌ ４中研究了一个双臂机器人的避碰规划算法的高阶逻辑形式化验证， 并根据验证结果改进了算法．本文的研究动机是在分数阶ＰＩＤ（ 比例Ｐｒｏｐｏｒｔｉ ｏｎ 、积分Ｉ ｎ ｔ ｅｇ ｒａｌ 、微分Ｄｅｒ ｉｖ ａｔ ｉ ｖｅ ） 控制系统高阶逻辑形式化验证的目标下产生的． 分数阶Ｐ Ｉ Ｄ 控制系统的高阶逻辑形式化验证， 需要分数阶拉普拉斯变换的相关理论和方法． 分数阶拉普拉斯变换是在拉普２ １ ２ ２ 计算机学报 ２ ０ ２ ０ 年拉斯变换基础上的拓展， 因此要对拉普拉斯变换基础内容性质定理进行高阶逻辑形式化验证． Ｗａ ｎｇ等人在Ｃｏ ｑ 中通过复变函数的形式化研究了拉普拉斯变换的形式化ｎ ｓ］． Ｔａ ｑｄ ｅｅ ｓ 等人在Ｈ Ｏ Ｌ Ｌｉ ｇｈ ｔ中通过多重微积分来验证拉普拉斯变换的形式化？ ３． 将拉普拉斯变换拓展到分数阶拉普拉斯变换， 需要用到函数极限的高阶逻辑形式化． Ｗｅｂ ｅ ｒ在Ｉ ｓ ａ ｂ ｅ ｌｌ ｅ ／ Ｈ （ ） Ｌ 中给出了函数在固定点处极限的定义［ １ ８］． 还有学者在Ｉ ｓ ａ ｂ ｅ ｌ ｌ ｅ ／ Ｈ Ｏ Ｌ 和Ｃｏｑ 中给出了函数极限的形式化研究［ １ ９ ２ １ １］， 但仅是函数趋于固定点的极限定义， 没有相关性质验证． 拉普拉斯变换拓展研究需要函数在正无穷大时极限， 及其相关性质属性等． 由于研究团队之前的分数阶微积分定义和性质等验证工作是建立在Ｈ Ｏ Ｌ 上的， 因此本文在Ｈ Ｏ Ｌ 中建立了函数在正无穷大时极限的定义和性质等定理， 以便后续工作的持续开展． 在高阶逻辑定理证明器Ｈ Ｏ Ｌ 中已包括一些基本定理库， 有实数库［２ １：， 超越函数库、自然数库［２２］、极限库［２ ３］、链表库［ ％ 等， 目前在Ｈ Ｏ Ｌ 中不存在函数在正无穷大时极限的高阶逻辑形式． 本文的验证基于首都师范大学团队研发的复数库［２３］、ｇ ａ ｕｇ ｅ 积分库和函数库中的一部分内容．３ 函数极限定义的建模与验证函数无穷远处极限： 设函数／ ： Ｄ Ｃ ｌ？ — Ｒ 是一个定义在实数上的函数， 并在某个开区间Ｕ ＞Ａ ｝ 上有定义． Ｌ 是一个给定的实数． 如果对任意的正实数￡， 都存在一个正实数Ｘ ， 使得对任意的实数Ｘ ， 只要？ｒ ＞ Ｘ ， 就有｜ ／（ ：ｒ ）— Ｌ｜那么就称Ｌ 是函数／在ｉ 趋于正无穷大时的极限， 或简称Ｌ 为／ 在正无穷处的极限， 记为ｌｉ ｍ ／（ ｘ ）＝ Ｌ 或／ （＿ｒ ）— Ａ （ ｘ—． ｒ ？ ｆ ？＋ 〇〇） ． 反之则称Ｌ 不是／ 在ｘ 趋于正无穷大时的极限．在Ｈ Ｏ Ｌ 中， 首先对实数域函数趋于正无穷的符号“―” 进行形式化描述， 给出如下定义：定义１． 函数无穷远处极限定义ｖ ａ ｌｔ ｅ ｎｄ ｓ ＿ ｒ ｅ ａ ｌ＿ ｒ ｅａ ｌ ＝Ｉ－＼ ／ ／ ／〇． ／— ／〇技（ ／ｔｅ ｎｄｓ ／０ ）（ ｍｔ ｏ ｐｍｒ ｌ ， ￥〉＝ ）定义中（ ／ ：  ｒ ｅａ ｌ—ｒ ｅａ ｌ ） 为实数域中要取正无穷极限的函数， （ ／〇：  ｒ ｅａ ｌ ） 则为该函数在正无穷远处的极限值． 而符号“―” 则用来表示中缀操作， 它的前项为要取无穷极限的实数域函数， 而它的后项则为该函数在无穷远处所取得的极限值． 因为Ｈ ＯＬ 中其它极限（ 包括序列极限以及函数在某点上极限） 的定义都使用等价于拓扑极限的方式， 所以在本文中也采用这种定义方式． 在拓扑学中， 网是序列的广义化， 用来统一极限不同的概念和将其广义至任意的拓扑空间． 根据拓扑中网极限的定义， 定义函数在实数域的极限． 式中ｔ ｅ ｎｄ ｓ 是网的定义， 后面则表示满足该网的一种条件． ｍ ｔｏ ｐ 为是将度量转换为拓扑的函数，ｍｒ ｌ 为实数直线上的度量定义， ￥＞＝ 则表示中缀操作， 是一个ｒ ｅ ａ 丨—ｒ ｅ ａ ｌ — ｂ ｏｏｌ 的集合运算符， 而这个集合中的所有元素都满足偏序关系， 这里主要用于确定取极限时的方向， 取负无穷时则会用￥２ ．根据上述对实数域函数在正无穷处取极限的形式化描述定义， 下面则对上述的定义进行形式化证明如下：定理１． 函数无穷远处极限ｖａ ｌＦ ＵＮ Ｃ＿Ｐ ＯＳ ＝ｈ Ｖ ／ｆ ０ ． ｆ－＊ ｆ０ ＜＾ ｙｅ ． ０ ＜ ｅ＾ ？ Ｘ． Ｖ ｘ． ｏ： ＞ ＆． Ｘ ＝＞ａ ｂ ｓ （ ／ ｘ 一／Ｏ Ｘｅ该定理等价符号的左边部分为实数域函数无穷极限的形式化定义， 右边部分为实数域函数在正无穷处极限的文字定义． 在这里， 利用Ｈ Ｏ Ｌ 的高阶逻辑对其进行形式化等价性证明．证明． 首先将符号“―” 进行重写， 用定义进行替换， 得到（ ／ｔ ｅ ｎｄ ｓ ／０ ） （ ｍ ｔｏ ｐ ｍｒ ｌ ， ￥＞＝ ） ， 然后通过度量拓扑中极限的特征定理ＭＴ ＯＰ ＿ Ｔ ＥＮＤ Ｓ对目标进行重写． 可将（ ／ ｔｅ ｎｄｓ ／Ｏ Ｋ ｍｔｏｐ￥＞＝）替换成一个类似等价符号右边的形式， 因为该定理就是将度量拓扑的定义展开， 并证明了集合满足某种关系， 这里即为偏序关系． 接着将实数域中的特殊函数类型及极限值类型用度量拓扑中的任意类型进行替换即可．对于上面的符号￥＞ ＝ 在集合域中满足有向集的关系， 这里将其以定理的形式给出证明， 以方便后面使用． 其高阶逻辑形式化证明如下：定理２． 集合有序关系ｖａｌ ＤＯ ＲＤ ＥＲ＿ＲＮ Ｇ Ｅ ＝Ｉ－ ｄｏｒｄ ｅｒ￥＞＝证明． ｄｏ ｒｄｅ ｒ 为Ｈ Ｏ Ｌ 系统中有向集合的定义． 在数学中， 有向集合（ 也叫有向预序或过滤集合）是一个具有序关系（ 自反及传递之二元关系〇的非空集合Ａ ， 而且每一对元素都会有个上界［ ２ ８ ］，亦即对于Ａ 中任意两个元素＾ 和６ ， 存在着Ａ 中的一个元素ｃ （ 不必然不同于ａ ， Ｗ ， 使得和赵春娜等： 函数极限的１ １ 期 高阶逻辑形式 化建模 与验证 ２ １ ２３（ 有向性） ． 有向集合是非空全序集合的一般化． 在拓扑中它们用来定义一般化序列的网， 并联合在数学分析中用到的各种极限的概念． 将ｄｏｒ ｄｅ ｒ 定义重写， 并且利用实数在关系￥＞＝ 上具有自反性的性质来证明． 会得到目标式子“？ ＆切八７ ＜ １￡／’， 若要证明《； 既大于：！ ： 又大于＾ ， 则需要证明Ｗ 大于Ｉ 中较大的一个即可． 因此再增加一个前件用来讨论当ｘ＞ｙ 时， 以及时的两种情况． 因此可以证明当工＞ ＾ 时， 取Ｚ 为：Ｃ 值； 当时， 取Ｚ 为＾ 值， 两种不同情况下都成立．对于实函数无穷极限取值的高阶逻辑形式化定义有：定义２ ． 实函数无穷极限值定义ｖａ ｌ ｆ＿ｌｉｍ ＝Ｉ－Ｖ ／． ｆ＿ｌｉｍ该定义的返回值并不是一个定义形式， 而是函数在正无穷远处的极限值， 这个定义将在后续形式化建模函数极限其它性质以及形式化拉普拉斯变换中会使用到． 实际控制系统的验证中还需要实函数在正无穷处取极限时的一些相关性质， 其形式化验证如下．４ 函数极限相关性质的建模与验证４． １ 基本性质（ １ ） 唯一性若极限ｌｉ ｍ ／（ ｘ ） 存在， 则此极限是唯一的． 其ｊ －＊ ｆ ■－〇形式化定理如下：定理３ ．唯一性ｖａ ｌＦＵＮ Ｃ＿ＵＮ Ｉ Ｑ ＝Ｖｘ ｘ ｌ—ｘ ｌ 八（ ｘ ｌ ＝ｘ ２ ）证明． 首先根据目标将定义的函数无穷极限的定义进行重写； 其次， 根据Ｈ Ｏ Ｌ 中度量拓扑中网的极限唯一性定理ＭＴＯ Ｐ＿Ｔ ＥＮ ＤＳ＿Ｕ Ｎ Ｉ Ｑ 进行Ｍ ＡＴＣ Ｈ 证明． 这时， 则需要证明关系集合： ￥＞＝是一个有向集． 这就是上面已经证明的定理２ ， 将之前证明的引理ＤＯＲ ＤＥＲ＿Ｒ ＮＧ Ｅ 进行ＭＡＴ Ｃ Ｈ 接收写入策略．证毕．（ ２ ） 保不等式性如果两个函数／， ｇ 在正无穷远处有极限， 即ｌ ｉ ｍ ／Ｃ ｒ ）＝ Ｌ ， ｌｉ ｍ ｇ （ ｘ ）＝ Ｍ， 并且在给定任意实Ｊ — ？ ４ － ＯＣ＋－ ■〇数ｅ ， 当： Ｔ＞ｅ 时， ／（ １ ） ＞ 尽（ ： ＊ ： ） ， 则有Ｌ ＞ Ｍ． 其形式化定理如下：定理４． 保不等式性ｖａ ｌ ＦＵ Ｎ Ｃ＿ＬＥ ＝＼－ ＼ｆｆ ｇ ｌｍ ．ｆ －＊－ｌ ｆ＼ ｇ＾－ ｍＡ（ ？ Ｘ ． Ｖ ｘ． ｊ： ＞ Ｘ ＝ ＞／ ｘｘ ）＝＞Ｋ ｍ证明． 首先使用Ｇ ＥＮ＿ Ｔ ＡＣ 将目标中的全称量词去掉； 其次需要使用Ｍ Ｐ＿ Ｔ ＡＣ 引人一个新的假设条件， 这个假设条件是度量拓扑中网的极限的比较定理Ｎ ＥＴ＿ＬＥ． 因为这个定理的形式是对任意类型的二元关系集合， 所以还需要使用ｇ ｅｑ （￥＞ ＝：ｒ ｅ ａｌ—ｒ ｅ ａ ｌ — ｂｏ ｏｌ ） 对该定理进行实例化关系类型，则最后使用的策略为：ＭＰ＿Ｔ Ａ Ｃ （ Ｉ Ｓ ＰＥ Ｃｇｅ ｑＮ ＥＴ＿ＬＥ ） ． 因为引人的前件是一个已经证明过的定理的实例化， 所以在此不需要进行证明， 可直接引人． 最后先使用ｔ ｅ ｎｄ ｓ＿ｒｅａ ｌ＿ｒ ｅ ａ ｌ 对目标中的函数在正无穷极限的定义进行重写； 然后使用ｇｅ ｑ 和有向集的定理Ｄ Ｏ ＲＤＥＲ＿Ｒ ＮＧ Ｅ 对目标进行重写， 再使用实数的自反性Ｒ ＥＡＬ＿ Ｌ Ｅ＿Ｒ Ｅ ＦＬ 对目标进行证明， 可得到跟前件的形式相似的目标； 最后使用匹配接收策略ＭＡ Ｔ ＣＨ＿ＡＣＣＥＰＴ＿ ＴＡ Ｃ 可完成证明． 证毕．（ ３ ） 极限为零如果函数／ 在无穷远处存在极限， 并且极限为零， 即ｌｉ ｍ／（ ：〇＝ ０ ， 则其绝对值函数在无穷远处＿ｒ ４－  ｃ的极限也为零， 即Ｉｌ ｉ ｍ ／（ ＿ｒ ）｜＝ ０ ， 反之也成立． 其． ｒ ＊＋形式化定理如下所示：定理５． 极限为零ｖａ ｌＦＵＮ Ｃ＿ＡＢＳ＝ｈＶ ／．  （Ａ ｘ ． ａ ｂｓ （ ／ ｊ： ） ）－？ ０ ＜＝＞ ／ －？ ０证明． 首先使用Ｇ ＥＮ ＿ ＴＡＣ 将目标中的全称量词去掉， 其次使用函数正无穷极限的定理Ｆ ＵＮＣ＿ＰＯ Ｓ 重写目标， 将会得到函数正无穷极限定义的形式目标． 接着使用Ｂ ＥＴＡ ＿ＴＡＣ 将目标中的Ａ函数去掉， 然后使用任意实数与零之间的差值关系定理ＲＥ Ａ Ｌ＿Ｓ ＵＢ＿ＲＺＥ ＲＯ 及任意实数的绝对值的绝对值与其绝对值相等的定理：ＡＢＳ＿ＡＢＳ 对目标进行重写即可证明完成．证毕．（ ４ ） 极限等价性若函数／ 在正无穷远处存在极限， 则该函数在正无穷远处的极限值为其在正无穷远处的取值．定理６ ． 极限等价性ｖａ ｌ ＬＩＭ＿ＦＵＮ Ｃ＿ＥＱ＝ｈ ＼／ｇ（ ｆ＿ ｌ ｉ ｍｆ＝ｌ ）证明． 该定理即是证明了之前定义的ｆ＿ｌ ｉ ｍ的正确性， 即当函数／ 在正无穷远处存在极限， 则２ １ ２ ４ 计算机学报 ２ ０ ２ ０ 年可推出ｆ＿ ｌｉ ｍ ／ 的值即是该函数的极限值． 首先将目标中的全称量词去掉并将ｆ＿ｌ ｉ ｍ 的定义进行重写， 因为ｆ＿ｌ ｉｍ 定义中使用了选择操作符＠ ， 所以在证明的时候需要使用消除选择操作符的策略：ＳＥＬＥＣＴ＿ＥＬＩＭ＿Ｔ Ａ Ｃ ， 将选择操作符＠ 变为存在（ ？ ） 和任意（ Ｖ ） 两个形式的目标． 此时可使用策略ＣＯ ＮＪ ＿Ｔ ＡＣ 将合取形式的目标分成两个子目标的形式． 两个子目标的前件都为函数／ 的正无穷处极限为“ 第一个子目标为证明存在一个实数ｘ 使得函数／ 的正无穷处的极限为该实数， 而第二个子目标则为对任意实数：ｒ 若函数／ 的极限为Ｉ ， 则ｘ 与Ｚ相等． 第一个子目标很好证明， 只需要将用／ 代替Ｘ ， 然后使用前件重写目标即可． 在第二个子目标中会发现， 函数／ 有两个正无穷极限值ｘ 和“ 然后需要证明ｚ 和／ 相等， 这与之前证明的函数在正无穷处的极限唯一性定理一致， 因此可以直接用自动证明策略ＰＲ 〇Ｖ Ｅ＿ＴＡ Ｃ ［Ｆ ＵＮ Ｃ＿ＵＮ Ｉ Ｑ］ （ 并将极限唯一性定理代入） 可完成证明．证毕．（ ５ ） 常函数极限若函数／ 为常函数， 则其在正无穷远处的极限值为函数本身．定理７ ． 常函数极限ｖ ａｌ ＦＵ Ｎ Ｃ＿ＣＯ Ｎ ＳＴ ＝ｈ Ｖ 々． （ Ａ ｘ ． 々）— 是．证明． 首先将目标中的全称量词去除， 然后用函数无穷极限的定理：Ｆ ＵＮＣ＿ ＰＯ Ｓ 对目标进行重写， 再分别使用定理：Ｒ ＥＡ Ｌ＿ＳＵＢ＿Ｒ ＥＦＬ 和ＡＢＳ＿０将目标中的“ａ ｂｓ Ｕ — 变为“０”． 此时的目标为：“ Ｖｅ ．０ ＜ ｅ＝＞？ Ｘ ． Ｖ ｘ ． ｘ ＞０ ＜ ｅ，，， 发现目标中的前件和结论都为“〇＜ｅ”， 那么就需要去除全称量词， 并使用策略ＤＩ ＳＣ Ｈ＿ＴＡ Ｃ 将目标中的前件放在条件队列中， 最后用自动重写策略ＡＳＭ ＿Ｒ ＥＷＲＩ Ｔ Ｅ＿Ｔ ＡＣ □ 即可完成证明．证毕．（ ６ ） 变量与常数之和的极限若函数／ 在正无穷远处存在极限， 即ｌ ｉ ｍ／（ ｘ ）＝ｊ － ＊４ － ｘＬ ， 则有任意常数ａ 使得下式成立：ｌ ｉｍ／（ ａ ＋ ｘ ）＝ Ｌ．其形式化描述：定理８． 变量与常数之和的极限ｖａ ｌＬＩＭ＿ＦＵ Ｎ Ｃ＿ＬＡ Ｍ＿ＡＤ Ｄ ＝Ｉ－Ｖ／ ／＋（ ７ ） 变量与常数之积的极限若函数／在正无穷远处存在极限， ８ 卩ｌｉｍ ／Ｏｒ ）＝Ｌ ， 则有任意常数ａ ＞０ 使得下式成立：ｌ ｉｍ ／（ ａ ＊ｘ ）＝Ｌ．其形式化描述：定理９． 变量与常数之积的极限ｖａ ｌＬ ＩＭ＿ ＦＵ ＮＣ＿ＬＡ Ｍ＿Ｍ ＵＬ ＝Ｉ－Ｖ ／／ ａ ． ａ￣＞ ０Ａ（ Ａ ｆ ． ／＜ ）－＊ ？／ （Ａ ｆ ． ／ （ ａ ＊这两个定理通过消去全称量词， 并用函数无穷极限的定理对目标重写即可证明．４． ２ 函数极限四则运算的建模与验证极限形式化语言只能证明极限， 不能求极限． 对于简单函数的极限问题， 可以使用比较容易的证明方法证明其极限存在或不存在， 但对于一些形式比较复杂的函数， 就不太容易证明． 因此， 函数正无穷极限的运算法则的形式化十分必要， 它对于证明复杂函数无穷极限的问题至关重要． 在上面正无穷极限的形式化模型的基础上， 这里将对正无穷极限的运算法则进行形式化建模及验证．在对函数在正无穷远处的极限的运算法则进行形式化描述和证明中， 形式化过程包括两种形式化内容．一种是在推出结果的形式中不带有而是使用“―” 的形式化， 这是最基本的形式化证明； 另外一种则是基于上一种证明的进一层， 是在推导结果中使用“＝” 和Ｕｉｍ 的形式， 而这种形式是在后面函数极限的应用形式化建模中所需要的． 如若跳过第一层形式的证明， 直接到第二层， 则会有很多证明代码的冗余． 因此， 为了能够更加有效地组织这些证明逻辑、过程以及代码形式， 最终抽出第一层形成单独的定理形式， 这样在后续的证明过程中可减少不必要的重复证明．（ １ ） 函数极限加法若函数／ 和ｇ 在正无穷远处都存在极限， 即ｌ ｉｍ ／（ ｘ ）＝ Ｌ ， 则有函数／和 ｇ的和在正无穷处存在极限并且：ｌ ｉｍ （ ／（ ｘ ） ＋ ＾ （ ｘ ） ）＝ Ｌ ＋Ｍ．其形式化描述：定理１ ０ ． 函数加法ｖａｌ ＦＵ ＮＣ＿Ａ ＤＤ ＝Ｉ＂＾ ｆ ｓｌｔ ＋ ｇｉ ｌ ＋ｍ＇） ．证明． 首先将全称量词去掉， 然后将ｔ ｅ ｎｄ Ｓ ＿ｒ ｅ ａｌ＿ｒ ｅａ ｌ 的定义进行重写， 去掉符号根据目标的形式使用ＭＡＴＣ Ｈ 策略匹配定理Ｎ ＥＴ＿ＡＤ Ｄ，目标会变成“ｄ ｏｒｄ ｅｒ￥＞＝”， 此时需要使用前面证赵春娜等： 函数极限的１ １ 期 高阶逻辑形式 化建模与验证 ２ １ ２５明过的定理２：Ｄ ＯＲ ＤＥＲ＿ＲＮＧＥ 来说明“￥＞＝”满足有向集关系， 用ＭＡＴ ＣＨ 接收策略将该定理代人即可．证毕．定理１ １ ． 函数极限加法ｖａ ｌ Ｌ ＩＭ＿ＦＵＮ Ｃ＿ＡＤ Ｄ ＝Ｉ－Ｖ／ ｇ／Ａ ｇ￣＞－ｍ ＾ （． ｉ＿ｌ ｉ ｍ （．Ｘ ｘ ． ｆ ｘ＋ ｇ ｘ ）＝Ｚ ＋ ？ｉ ） ．证明． 由于极限的运算是用ｆ＿ Ｈｍ 定义写的，所以首先去除全称量词及重写Ｕｉ ｍ 的定义， 由于ｆ＿ｌｉ ｍ 定义中使用了选择操作运算符＠ ， 因此证明需要使用策略ＳＥ ＬＥＣＴ ＿ＥＬＩＭ＿ Ｔ Ａ Ｃ ， 这样就可以将目标转换为两个目标的合取形式，一个是证明存在性，一个证明等价性． 使用ＣＯ ＮＪ ＿Ｔ ＡＣ 将目标中的合取形式变为两个子目标． 第一个子目标， 是证明两个函数的和在无穷远处存在极限， 根据前件中的条件函数／ 和ｇ 在无穷远处的极限分别为Ｚ 和因此只需要证明两个函数的和在正无穷远处的极限值为Ｚ ＋ ｍ 即可． 那么就需要ＭＡＴ ＣＨ ＿ ＭＰ＿ Ｔ ＡＣ 对上面已经证明完的定理ＦＵ ＮＣ＿ＡＤＤ 进行匹配， 然后重写目标即可． 第二个子目标， 去掉全称量词后发现它的目标形式与之前证明函数极限的唯一性定理ＦＵＮ Ｃ＿ Ｕ ＮＩ Ｑ 很相似？ 此时需要使用Ｍ Ａ ＴＣ Ｈ 策略匹配该定理， 则目标变成了“？乂ｘＡ ｉ—Ｇ ＋ ｍ ）” 的形式． 先证明目标合取式的第一部分， 即证明存在性， 显然存在的Ｖ 应该为（ Ａｉ． ／ ｘ ＋ ｇ Ｊ： ） ，所以根据前件的条件可以消去目标合取式的第一部分； 而目标的第二部分与上面第一层证明极限和的形式一样， 所以使用ＭＡＴＣ Ｈ 策略匹配定理ＦＵＮ ＣＬＡＤＤ 即可．证毕．（ ２ ） 函数极限减法若函数／ 和ｇ 在正无穷远处都存在极限， 即ｌ ｉｍ ／（ ｘ ）＝ Ｌ ， ｌ ｉ ｍ 尽（ ＿ｒ ）＝ Ｍ， 则有函数／ 和莒的Ｘ －＊＋ ＝Ｃ＋ＣＣ差在正无穷处存在极限并且：ｌ ｉｍ＋ ｏ ｃ其形式化描述：定理１ ２． 函数减法ｖ ａ ｌＦ ＵＮＣ＿ＳＵ Ｂ＝Ｎｆｇｌ ｍ． ｆ一ｌｔ—ｇ该定理的证明方法与定理１ ０ 是类似的．定理１３ ． 函数极限减法ｖａ ｌ ＬＩＭ＿ Ｆ ＵＮ Ｃ＿ＳＵ Ｂ＝ｌ—ｍ ） ．该定理的证明方法与定理１ １ 是类似的．（ ３ ） 函数极限乘法若函数／ 和ｇ 在正无穷远处都存在极限， 即ｌ ｉ ｍ ／（ ｘ ）＝ Ｌ ， ｌ ｉｍ ｇ （ ｘ ）＝ Ｍ， 则有函数／和ｇ？ 的Ｘ －＊积在正无穷处存在极限并且：ｌ ｉ ｍ （ ／ （ ｘ ）Ｘ ＾（ ｘ ） ）＝ Ｌ Ｘ Ｍ．Ｊ －＊ ＋ＯＯ其形式化描述：定理１ ４ ． 函数乘法ｖａ ｌ Ｆ ＵＮ Ｃ＿Ｍ ＵＬ ＝ｆｇｌｍ ． ｆ—ｌｔ＊ ｇｔ ｌ— Ｕ＊ ｍ ） ．定理Ｉ Ｓ ． 函数极限乘法ｖａ ｌ ＬＩＭ＿ＦＵ Ｎ Ｃ＿ＭＵＬ＝卜Ｖ ／ ｇＺｍ． ／—Ｚ Ａ ｇ—ｍ ＝＞ （ ｆ＿ｌ ｉｍ （ Ａｘ． ／ ｘ＊ｇ ｘ ）＝ｌ ＊ ｍ） ．证明． 通过使用策略ＳＥＬＥＣＴ＿Ｅ ＬＩＭ ＿ＴＡＣ ，可以将目标转换为两个目标的合取形式，一个是证明存在性，一个证明等价性． 使用ＣＯ ＮＪ ＿ＴＡＣ 将目标中的合取形式变为两个子目标． 第一个子目标， 是证明两个函数的乘积在无穷远处存在极限． 根据前件中的条件函数／ 和ｇ 在无穷远处的极限分别为Ｚ和？ｎ ， 因此只需要证明两个函数的和在正无穷远处的极限值为ｍ Ｘ Ｚ 即可． 那么就需要Ｍ Ａ ＴＣＨ ＿ＭＰ＿ＴＡＣ 对上面已经证明完的定理Ｆ ＵＮＣ＿ＭＵ Ｌ 进行匹配， 然后重写目标即可． 第二个子目标， 需要使用ＭＡＴ ＣＨ 策略匹配该定理， 则目标变成了“？—ｘ 八ｘ＇— 的形式， 先证明目标合取式的第一部分， 证明存在性， 显然存在的ｘ＇ 应该为（ Ａ ｏ ｒ ． ／ ｉ＊ｇ ｘ ） ， 所以根据前件的条件可以消去目标合取式的第一部分； 目标的第二部分使用ＭＡＴＣ Ｈ 策略匹配定理Ｆ Ｕ Ｎ Ｃ＿ＭＵ Ｌ 即可证明．证毕．（ ４ ） 函数极限与常数乘法若函数／ 在正无穷远处存在极限， 即ｌ ｉｍ／Ｕ ）＝Ｌ ， 则有任意常数ａ ， 使得ａ 与／ 的乘积在正无穷处存在极限并且：ｌｉｍ ａ Ｘ ／（ ｘ ）＝ ａ Ｘ Ｌ．其形式化描述：定理１ ６ ． 函数极限与常数乘法ｖ ａｌ ＬＩＭ＿ＦＵ Ｎ Ｃ＿ＣＭ ＵＬ＝ｈ Ｖ／ １ ａ ． ｆ＾￣ｌ＝＞（ ｆ＿ｌ ｉｍ （Ａ ｘ． ａ＊ｆ ｘ ）＝ ａ＊Ｖ） ： ｔｈｍ．证明． 由于该目标的形式与上一个定理： 函数极限的乘法运算很相似， 因此可以借助定理： ＬＩＭ＿２ １ ２ ６ 计算机学报 ２ ０ ２ ０年ＦＵ ＮＣ＿ＭＵ Ｌ 来进行证明． 那么就需要将目标的形式变成与所用定理一样的形式， 在定理ＬＩＭ＿ ＦＵＮＣ＿Ｍ ＵＬ 中， 是两个函数乘积的形式， 而在证明目标中则是一个常数与一个函数的乘积形式， 因此需要使用定位策略及添加ｌ ａｍ ｂ ｄａ 函数的方法将常数改写为常函数的形式： ＣＯ ＮＶ ＿ ＴＡ Ｃ （ （ Ｌ Ａ ＮＤ ＿ＣＯＮ Ｖ〇ＥＸＡＣＴ—ＣＯＮ Ｖ） ［ Ｘ ＿ ＢＥＴＡ＿ ＣＯＮＶ （—‘ｘ ： ｒ ｅａ ｌ，－－）（－‘ａ ：ｒ ｅａ ｌ’－ －） ］ ） ． 应用到要证明的定理中， 则左侧即可表示为， 对目标中的常数ａ 添加一个自变量为？ｒ 的ｌ ａｍｂ ｄ ａ 函数． 此时的目标形式为：ｆ＿ｌ ｉｍ （ Ａ ｘ ．（ Ａ ｘ ． ａ ）〇： ）＝ ？ ＊ ／？ 此时便可以使用Ｍ Ａ ＴＣ Ｈ策略匹配定理ＬＩＭ＿ Ｆ ＵＮＣ ＿ＭＵ Ｌ ， 然后使用常函数极限定理ＦＵＮ Ｃ ＿ＣＯ ＮＳＴ 进行重写， 即可完成证明．证毕．（ ５ ） 函数极限除法若函数／ 和ｇ 在正无穷远处都存在极限， 即ｌ ｉｆ／（ ｘ ）＝ Ｌ ， ｌｉ ｉｊｉ ｇ （ ＿ｒ ）＝ Ｍ， 并且Ｍ尹０ ， 则有函ｋ ／ 和ｇ 的商ｉ正无穷处存在极限并且：Ｋ（ ｆＵ ） ／ ｇ Ｕ） ）＝ Ｌ ／Ｍ．其形式ｉ描述：定理１ ７ ． 函数极限除法ｖａ ｌ ＦＵＮ Ｃ＿ＤＩＶ ＝Ｎ ｆｇｌｈ ｇ— ｍｉ Ｘ ｔ ． ｆｔ／ ｇ证明． 首先将全称量词去掉， 然后将ｔ ｅ ｎｄ Ｓ ＿ｒｅ ａＬｒ ｅ ａ ｌ 的定义进行重写， 去掉符号“—”， 根据目标的形式使用ＭＡＴ ＣＨ 策略匹配定理Ｎ ＥＴ＿ ＤＩＶ， 目标会变成“ｄｏｒ ｄｅ ｒ￥＞＝”， 此时需要使用前面证明过的定理２ ： Ｄ ０Ｒ ＤＥＲ＿ＲＮＧ Ｅ 来说明“￥＞＝”满足有向集关系， 即用ＭＡＴＣＨ 接收策略将该定理代人即可．证毕．４ ． ３ 函数积分极限的高阶逻辑形式化建模与验证（ １ ） 正无穷函数积分上限取绝对值的建模与验证若函数／ 在以任意常数ａ 为积分下限存在正无穷积分Ｌ ， 即ｌ ｉ ｍｆＶ（ ｘ ）＝ Ｌ ， 则有该函数在以＾ｊ－ ＊ ＋＜？Ｊ ａ为积分下限， 积分上限为取正无穷变量的绝对值的极限为Ｌ ， 即ｐ１ｌ ｉｍ／ （ ｘ）＝ Ｌ ．ｘ －＾ ＋〇〇Ｊ ａ该定理表示， 函数积分上限取极限时， 与其上限的绝对值取极限的结果一样． 其形式化描述如下：定理１８ ． 函数积分极限上限绝对值定理ｖａ ｌ ＬＩＭ＿ＦＵＮＣ＿ＢＯ ＵＮＤ＿ＡＢ Ｓ ＝１－ Ｖ／ ａ ／＞．  （ Ａ ＾ ． ｉ ｎｔ ｅ ｇｒａｌ （ ａ ， ｉ ）（ Ａ ？ ． ｉ ｎｔ ｅ ｇｒ ａ ｌ（ ａ ，ａ ｂ ｓｆ ）证明． 首先用极限定理ＦＵＮＣ＿ＰＯ Ｓ 重写， 然后使用等价策略（ ＥＱ＿ ＴＡＣ ） 将等价性证明变换成两个蕴含式证明． 第一个子目标的蕴含式证明： 由于目标中存在两个蕴含式且它们之间的关系为蕴含关系， 每个蕴含式中都有一个〇所以先将两个ｅ 实例化为同一个ｅ ， 主要使用ＳＰＥＣ ， 即ＭＰ＿ ＴＡＣ〇 ＳＰＥＣ“ｅ ： ｒｅ ａｒ． 目标式中有存在量词的证明， 实际上在０＜ ？ 时， ａ ｂｓ． 所以， 两个蕴含式中的Ｘ ， 即存在量词， 可以写成一个？ 此时， 目标变为“ａ ｂ ｓ （ ｉ ｎｔ ｅｇ ｒａｌ（ ａ ， ａ ｂ ｓｊ： ）而前件中有三个条件分别为“工Ｘ ”，“ Ｖｘ ． ＿ｒ＞ ＆ Ｘ＞ａ ｂ ｓ（ ｉ ｎ ｔｅ ｇ ｒａ ｌ （ ａ ， ｘ ）／—／＞） ＜， 和“ＯＯ ”． 从条件２ 中可以发现， 其成立的条件为“ｚ ＞对目标来说， 它的成立条件形式应该为“ａｂｓ＆ Ｘ”． 所以使用目标中的前件匹配结果， 即可得到目标： ａ ｂｓ ： ｒ ＞ ＆ Ｘ ， 经过简单的变换， 根据条件即可完成第一个子目标的证明．第二个子目标的证明思路与第一个子目标很相似， 但第二个子目标中的蕴含式与第一个子目标中的蕴含式刚好相反， 条件和结果进行了调换， 所以在证明到目标形式为“ａ ｂ ｓ （ ｉ ｎｔ ｅｇ ｒａｌ （ ａ ， ：ｃ ） ／ ＿ｐ ） ＜ ｅ”的时候， 有所不同． 此时的前件条件中有“ｘ ＞ ＆ Ｘ ”，ＭＶｏ ： ． ｘ ＞ ＆－ Ｘ ＝＞ａ ｂｓ （ ｉｎ ｔ ｅｇ ｒａ ｌ （ ａ ，ａ ｂｓ ｘ ） ｆ￣ｐ＇） ＜ｉ ｅｎ和“０ ＜ ， ． 此时条件２ 中的目标中有“ａ ｂ ｓ的形式， 而条件中的前件却为并没有绝对值ａ ｂ ｓ 的形式． 而目标中也没有绝对值ａｂｓ 的使用． 为了能使用前件中第二个条件， 需要将目标的形式改写为与前件第二个条件的目标相似的形式． 即用ａ ｂ ｓ ｉ 代替目标中的Ｘ ， 将目标变为“ａｂ ｓ （ ｉ ｎｔ ｅ ｇｒａｌＵ ，ａ ｂ ｓｚ ） ／＿／＞ ） ＜ ，． 而前件中第一个条件为“ｘ ＞ ＆ Ｘ”，： ｃ 为实数， 而Ｘ 为自然数， 因此会有“ ＆ Ｘ” 的形式， 是将自然数取实数的表示方法． 由此可知， 若一个实数大于等于一个自然数， 那么这个实数与其绝对值是相等的．证明步骤如下：首先证明“〇＜ ｘ”， 需要使用实数小于等于的传递定理ＲＥＡＬ＿ＬＥ＿ＴＲＡＮＳ ， 找到一个处于０ 和ｘ 的中间值， 那就是自然数兄于是分别证明“和“０２ Ｘ”， 第一个目标用重写即可（ 前件条件中有该目标的形式） ． 第二个目标使用定理Ｚ ＥＲ〇＿ ＬＥＳＳ＿ＥＱ （ 表示自然数不小于零） 即可证明．其次证明“ｘ＝ ａｂ ｓＩ”， 使用定理ＡＢＳ＿ ＲＥＦＬ（ 实