欢迎访问一起赢论文辅导网
本站动态
联系我们

手机:15327302358
邮箱:peter.lyz@163.com

Q Q:
910330594  
微信paperwinner
工作时间:9:00-24:00

SCI期刊论文
当前位置:首页 > SCI期刊论文
函数极限的高阶逻辑形式化建模与验证_赵春娜
来源:一起赢论文网     日期:2021-05-28     浏览数:1381     【 字体:

 引言人工智能一直是科技界的一个努力方向, 能够与人类互动的机器人更是人们研究的热点之一.2 0 1 5 年7 月, 德国大众工厂发生“ 机器人杀人”事件.提高机器人的可靠性和安全性是机器人应用的至关重要的问题. 机器人系统的可靠性主要依赖于其控制系统. 形式化方法是基于数学方法描述目标系统属性的一种技术, 它提供了更完备的验证结果, 为交互式机器人的安全验证提供了坚实的基础. 髙阶逻辑定理证明方法是形式化方法中一种严谨的验证方法. 在高阶逻辑定理证明方法中, 机器人核心控制系统的验证需要很多定理库的支持, 其中拉普拉斯变换的形式化是一个重要的内容. 拉普拉斯变换的形式化是以函数极限和相关性质的高阶逻辑形式化为基础的.函数极限是数学中的基本概念之一, 也是拉普拉斯变换等的理论基础, 本文在高阶逻辑定理证明器中研究了函数正无穷大时极限及相关性质的形式化建模和验证, 为控制系统的高阶逻辑验证提供基础理论. 第2 节介绍高阶逻辑定理证明器; 第3 节建立函数正无穷大时极限的高阶逻辑模型; 第4 节对函数极限的基本性质、四则运算和函数积分极限的一些性质进行形式化建模和验证; 第5 节对拉普拉斯变换卷积定理建立高阶逻辑形式化模型; 第6 节应用本文的内容对电阻- 电感电路( 简称RL 电路)中的电流进行高阶逻辑形式化建模与验证.2 高阶逻辑定理证明器定理证明是形式化方法的一种, 它是一种用数学逻辑公式来表达系统及其属性的技术, 通过对现实中的物理模型提取属性性质转换为数学模型, 再由数学模型转换为逻辑模型, 并在相关定理证明器中进行描述, 从而得到一个形式化系统, 找到某属性的一个证明过程. 定理证明是一种交互式分析技术.它的分析原理是为系统的需求规范和设计实现建立逻辑模型, 然后通过形式化定理验证两者的关系. 如果该定理通过证明是正确的, 则说明实现和需求之间是等价的或是蕴含的. 定理证明克服了等价性验证需要建立标准模型和模型检测处理复杂系统会产生空间爆炸的约束的问题. 由于定理证明器可以表达所有可以逻辑化的东西, 它已用于多个领域的可靠性分析, 如应用高阶逻辑来验证操作系统的安全需求[ S赵春娜等: 函数极限的1 1 期 高阶逻辑形式化建模与验证 2 1 2 1文献[2] 用高阶逻辑表达线性时态逻辑和区间时态逻辑, 并以实例说明它在硬件设计验证中的应用;应用定理证明也可以来验证多机器人路径规划的安全性文献[4] 在高阶逻辑证明工具H O L- L i gh t中建立了几何代数系统的形式化模型等等. 定理证明虽然可以表达所有可逻辑化的系统, 但是证明定理时需要人工引导, 于是要求定理证明器的使用者熟悉逻辑推理并且拥有一定的推理经验, 这是定理证明难以大众化的原因. 目前, 定理证明主要应用于一些系统关键性质的分析, 在特殊领域里定理证明发挥了巨大优势. 定理证明技术逐渐成为形式化验证技术的重点研究方向, 在研究和应用上都拥有巨大的发展潜力?定理证明本质是, 基于系统的公理及推导规则来为定理寻找证明[5]. 当演绎推理和数学定理的手工推导证明, 变化成为符号演算的过程技术, 并且可以在计算机上自动进行时, 定理证明就成为当今软件工程领域中一种非常重要的形式验证技术[ 6], 即定理证明系统. 在运用定理证明的方法进行系统设计验证时, 辅助手工推导的计算机程序被称为机械定理证明器, 它和自动定理证明器组成了自动化程度不同的定理证明器. 现在, 具有各种特点的定理证明系统已成为教育、学术及工业界的有力工具. 这些定理证明系统拥有各种不同的特性, 主要系统有A CL2 、C oq 、Leg o 、Is a be l l e 、H O L和 P VS等?A CL2是由早期用于软件验证的定理证明器Bo ye r-M oore发展来的, A CL2 从设计上支持基于归纳逻辑理论的自动推理, 可应用于软件或硬件系统的验证.ACL2 定理证明器的核心是基于项重写系统. Coq支持数学断言的表达式, 机械化地对这些断言执行检查, 辅助寻找正式证明, 并从其形式化描述的构造性证明中提取出可验证的程序. Coq 基于归纳构造演算, 是构造演算的一种衍生理论.H O L ( Hi g he r- 〇rde r Log i c ) 是定理证明中的高阶逻辑定理证明器, 由G ord on 于2 0 世纪8 0 年代中期在英国剑桥大学创建的高阶逻辑系统[ 7 8 ], 其主要特点是通过M L ( M e ta L a n gu ag e 是一个通用的函数式编程语言) 语言实现高度的可编程性. 本文采用的版本是HO L4 , 该工具是利用缜密的数学逻辑来实现工业验证的精确性. M L 是一种强类型函数程序设计语言, 是比较经典的函数式语言, 其所有对象的类型都必须在编译的时候静态分析决定.ML 提供的类型有单元( u ni t ) 、布尔型( bo ol ) 、整型( i n t ) 、字符串型( s t r i ng ) 、实数( r e a l ) 、元组( t u p l e ) 、记录( r e co rd) 和列表( l i s t ) . ML 还支持模式匹配、意外处理、类型引用、多态性以及递归数据结构. 它拥有自然的语法和较少的基本概念, 其理论基础是A演算, 语言实现严谨、高效且易于理解, 用户可以容易写出清晰可靠的程序. 大多数著名的推理系统都是用M L 语言编写的. M L 语言作为一种函数式编程语言, 减少了指针的使用, 并提供了灵活的表达方式, 有助于管理复杂的对象. ML 编译器循环地进行“输入-求值-输出”, 用户标准的操作方式是一条一条地输人M L 表达式或者声明, 让M L 编译器去处理. M L 编译器处理的过程包括类型检査、编译、执行. M L 家族有好几种语言, 主要的两种语言是Ca m l 和标准ML , 标准M L 语言被简称为SML , 或者直接称为ML .ML 语言结合了函数式编程语言和命令式编程语言的特点, 这是它得以广泛应用的重要原因.在定理证明器H O L4 中进行形式化证明时, 如要使用定理库里相关的定义和定理, 需要先用l oa d和o pe n 语句加载并打开相应的定理库. HO L 4 有非常丰富的定理库, 并且由于其庞大的用户基础, 定理库会越来越丰富. 随着H O L4 定理库越来越完善, 其应用也越来越广泛. 加拿大Con co rd ia 大学的S i dd iq u e 等人在高阶逻辑定理证明器H O L 中验证了分数阶微积分RL 定义[9] 和G a mm a 函数[ 1 "]; Li u等人在髙阶逻辑定理证明器HO L 中验证了马尔科夫链[1 1 ], 为系统的状态验证提供基础. K uma r 等人利用H O L 分析了D N A 中的纳米生物规模的化学信息处理动态D 2], 开发利用全息理解分子尺度生物化学计算行为的新形式. A h me d 等人在HOL 中对可靠性框图进行了形式化验证[1 3], 对串并联、平行、嵌套等建立了形式化模型, 并验证了云计算中心的一个通用的虚拟数据的可靠性. 巴基斯坦的S a r da r等人对于分布式动态热管理系统, 应用高阶逻辑方法验证系统的性能和时间属性[ M ], 包括热性能、温度范围、达到热稳定性时间等. 文献[ 1 5] 在HO L 4中研究了一个双臂机器人的避碰规划算法的高阶逻辑形式化验证, 并根据验证结果改进了算法.本文的研究动机是在分数阶PID( 比例Proporti on 、积分I n t eg ral 、微分Der iv at i ve ) 控制系统高阶逻辑形式化验证的目标下产生的. 分数阶P I D 控制系统的高阶逻辑形式化验证, 需要分数阶拉普拉斯变换的相关理论和方法. 分数阶拉普拉斯变换是在拉普2 1 2 2 计算机学报 2 0 2 0 年拉斯变换基础上的拓展, 因此要对拉普拉斯变换基础内容性质定理进行高阶逻辑形式化验证. Wa ng等人在Co q 中通过复变函数的形式化研究了拉普拉斯变换的形式化n s]. Ta qd ee s 等人在H O L Li gh t中通过多重微积分来验证拉普拉斯变换的形式化? 3. 将拉普拉斯变换拓展到分数阶拉普拉斯变换, 需要用到函数极限的高阶逻辑形式化. Web e r在I s a b e ll e / H ( ) L 中给出了函数在固定点处极限的定义[ 1 8]. 还有学者在I s a b e l l e / H O L 和Coq 中给出了函数极限的形式化研究[ 1 9 2 1 1], 但仅是函数趋于固定点的极限定义, 没有相关性质验证. 拉普拉斯变换拓展研究需要函数在正无穷大时极限, 及其相关性质属性等. 由于研究团队之前的分数阶微积分定义和性质等验证工作是建立在H O L 上的, 因此本文在H O L 中建立了函数在正无穷大时极限的定义和性质等定理, 以便后续工作的持续开展. 在高阶逻辑定理证明器H O L 中已包括一些基本定理库, 有实数库[2 1:, 超越函数库、自然数库[22]、极限库[2 3]、链表库[ % 等, 目前在H O L 中不存在函数在正无穷大时极限的高阶逻辑形式. 本文的验证基于首都师范大学团队研发的复数库[23]、g a ug e 积分库和函数库中的一部分内容.3 函数极限定义的建模与验证函数无穷远处极限: 设函数/ : D C l? — R 是一个定义在实数上的函数, 并在某个开区间U >A } 上有定义. L 是一个给定的实数. 如果对任意的正实数£, 都存在一个正实数X , 使得对任意的实数X , 只要?r > X , 就有| /( :r )— L|那么就称L 是函数/在i 趋于正无穷大时的极限, 或简称L 为/ 在正无穷处的极限, 记为li m /( x )= L 或/ (_r )— A ( x—. r ? f ?+ 〇〇) . 反之则称L 不是/ 在x 趋于正无穷大时的极限.在H O L 中, 首先对实数域函数趋于正无穷的符号“―” 进行形式化描述, 给出如下定义:定义1. 函数无穷远处极限定义v a lt e nd s _ r e a l_ r ea l =I-\ / / /〇. /— /〇技( /te nds /0 )( mt o pmr l , ¥〉= )定义中( / :  r ea l—r ea l ) 为实数域中要取正无穷极限的函数, ( /〇:  r ea l ) 则为该函数在正无穷远处的极限值. 而符号“―” 则用来表示中缀操作, 它的前项为要取无穷极限的实数域函数, 而它的后项则为该函数在无穷远处所取得的极限值. 因为H OL 中其它极限( 包括序列极限以及函数在某点上极限) 的定义都使用等价于拓扑极限的方式, 所以在本文中也采用这种定义方式. 在拓扑学中, 网是序列的广义化, 用来统一极限不同的概念和将其广义至任意的拓扑空间. 根据拓扑中网极限的定义, 定义函数在实数域的极限. 式中t e nd s 是网的定义, 后面则表示满足该网的一种条件. m to p 为是将度量转换为拓扑的函数,mr l 为实数直线上的度量定义, ¥>= 则表示中缀操作, 是一个r e a 丨—r e a l — b ool 的集合运算符, 而这个集合中的所有元素都满足偏序关系, 这里主要用于确定取极限时的方向, 取负无穷时则会用¥2 .根据上述对实数域函数在正无穷处取极限的形式化描述定义, 下面则对上述的定义进行形式化证明如下:定理1. 函数无穷远处极限va lF UN C_P OS =h V /f 0 . f-* f0 <^ ye . 0 < e^ ? X. V x. o: > &. X =>a b s ( / x 一/O Xe该定理等价符号的左边部分为实数域函数无穷极限的形式化定义, 右边部分为实数域函数在正无穷处极限的文字定义. 在这里, 利用H O L 的高阶逻辑对其进行形式化等价性证明.证明. 首先将符号“―” 进行重写, 用定义进行替换, 得到( /t e nd s /0 ) ( m to p mr l , ¥>= ) , 然后通过度量拓扑中极限的特征定理MT OP _ T END S对目标进行重写. 可将( / te nds /O K mtop¥>=)替换成一个类似等价符号右边的形式, 因为该定理就是将度量拓扑的定义展开, 并证明了集合满足某种关系, 这里即为偏序关系. 接着将实数域中的特殊函数类型及极限值类型用度量拓扑中的任意类型进行替换即可.对于上面的符号¥> = 在集合域中满足有向集的关系, 这里将其以定理的形式给出证明, 以方便后面使用. 其高阶逻辑形式化证明如下:定理2. 集合有序关系val DO RD ER_RN G E =I- dord er¥>=证明. do rde r 为H O L 系统中有向集合的定义. 在数学中, 有向集合( 也叫有向预序或过滤集合)是一个具有序关系( 自反及传递之二元关系〇的非空集合A , 而且每一对元素都会有个上界[ 2 8 ],亦即对于A 中任意两个元素^ 和6 , 存在着A 中的一个元素c ( 不必然不同于a , W , 使得和赵春娜等: 函数极限的1 1 期 高阶逻辑形式 化建模 与验证 2 1 23( 有向性) . 有向集合是非空全序集合的一般化. 在拓扑中它们用来定义一般化序列的网, 并联合在数学分析中用到的各种极限的概念. 将dor de r 定义重写, 并且利用实数在关系¥>= 上具有自反性的性质来证明. 会得到目标式子“? &切八7 < 1£/’, 若要证明《; 既大于:! : 又大于^ , 则需要证明W 大于I 中较大的一个即可. 因此再增加一个前件用来讨论当x>y 时, 以及时的两种情况. 因此可以证明当工> ^ 时, 取Z 为:C 值; 当时, 取Z 为^ 值, 两种不同情况下都成立.对于实函数无穷极限取值的高阶逻辑形式化定义有:定义2 . 实函数无穷极限值定义va l f_lim =I-V /. f_lim该定义的返回值并不是一个定义形式, 而是函数在正无穷远处的极限值, 这个定义将在后续形式化建模函数极限其它性质以及形式化拉普拉斯变换中会使用到. 实际控制系统的验证中还需要实函数在正无穷处取极限时的一些相关性质, 其形式化验证如下.4 函数极限相关性质的建模与验证4. 1 基本性质( 1 ) 唯一性若极限li m /( x ) 存在, 则此极限是唯一的. 其j -* f ■-〇形式化定理如下:定理3 .唯一性va lFUN C_UN I Q =Vx x l—x l 八( x l =x 2 )证明. 首先根据目标将定义的函数无穷极限的定义进行重写; 其次, 根据H O L 中度量拓扑中网的极限唯一性定理MTO P_T EN DS_U N I Q 进行M ATC H 证明. 这时, 则需要证明关系集合: ¥>=是一个有向集. 这就是上面已经证明的定理2 , 将之前证明的引理DOR DER_R NG E 进行MAT C H 接收写入策略.证毕.( 2 ) 保不等式性如果两个函数/, g 在正无穷远处有极限, 即l i m /C r )= L , li m g ( x )= M, 并且在给定任意实J — ? 4 - OC+- ■〇数e , 当: T>e 时, /( 1 ) > 尽( : * : ) , 则有L > M. 其形式化定理如下:定理4. 保不等式性va l FU N C_LE =\- \ff g lm .f -*-l f\ g^- mA( ? X . V x. j: > X = >/ xx )=>K m证明. 首先使用G EN_ T AC 将目标中的全称量词去掉; 其次需要使用M P_ T AC 引人一个新的假设条件, 这个假设条件是度量拓扑中网的极限的比较定理N ET_LE. 因为这个定理的形式是对任意类型的二元关系集合, 所以还需要使用g eq (¥> =:r e al—r e a l — bo ol ) 对该定理进行实例化关系类型,则最后使用的策略为:MP_T A C ( I S PE Cge qN ET_LE ) . 因为引人的前件是一个已经证明过的定理的实例化, 所以在此不需要进行证明, 可直接引人. 最后先使用t e nd s_rea l_r e a l 对目标中的函数在正无穷极限的定义进行重写; 然后使用ge q 和有向集的定理D O RDER_R NG E 对目标进行重写, 再使用实数的自反性R EAL_ L E_R E FL 对目标进行证明, 可得到跟前件的形式相似的目标; 最后使用匹配接收策略MA T CH_ACCEPT_ TA C 可完成证明. 证毕.( 3 ) 极限为零如果函数/ 在无穷远处存在极限, 并且极限为零, 即li m/( :〇= 0 , 则其绝对值函数在无穷远处_r 4-  c的极限也为零, 即Il i m /( _r )|= 0 , 反之也成立. 其. r *+形式化定理如下所示:定理5. 极限为零va lFUN C_ABS=hV /.  (A x . a bs ( / j: ) )-? 0 <=> / -? 0证明. 首先使用G EN _ TAC 将目标中的全称量词去掉, 其次使用函数正无穷极限的定理F UNC_PO S 重写目标, 将会得到函数正无穷极限定义的形式目标. 接着使用B ETA _TAC 将目标中的A函数去掉, 然后使用任意实数与零之间的差值关系定理RE A L_S UB_RZE RO 及任意实数的绝对值的绝对值与其绝对值相等的定理:ABS_ABS 对目标进行重写即可证明完成.证毕.( 4 ) 极限等价性若函数/ 在正无穷远处存在极限, 则该函数在正无穷远处的极限值为其在正无穷远处的取值.定理6 . 极限等价性va l LIM_FUN C_EQ=h \/g( f_ l i mf=l )证明. 该定理即是证明了之前定义的f_l i m的正确性, 即当函数/ 在正无穷远处存在极限, 则2 1 2 4 计算机学报 2 0 2 0 年可推出f_ li m / 的值即是该函数的极限值. 首先将目标中的全称量词去掉并将f_l i m 的定义进行重写, 因为f_l im 定义中使用了选择操作符@ , 所以在证明的时候需要使用消除选择操作符的策略:SELECT_ELIM_T A C , 将选择操作符@ 变为存在( ? ) 和任意( V ) 两个形式的目标. 此时可使用策略CO NJ _T AC 将合取形式的目标分成两个子目标的形式. 两个子目标的前件都为函数/ 的正无穷处极限为“ 第一个子目标为证明存在一个实数x 使得函数/ 的正无穷处的极限为该实数, 而第二个子目标则为对任意实数:r 若函数/ 的极限为I , 则x 与Z相等. 第一个子目标很好证明, 只需要将用/ 代替X , 然后使用前件重写目标即可. 在第二个子目标中会发现, 函数/ 有两个正无穷极限值x 和“ 然后需要证明z 和/ 相等, 这与之前证明的函数在正无穷处的极限唯一性定理一致, 因此可以直接用自动证明策略PR 〇V E_TA C [F UN C_UN I Q] ( 并将极限唯一性定理代入) 可完成证明.证毕.( 5 ) 常函数极限若函数/ 为常函数, 则其在正无穷远处的极限值为函数本身.定理7 . 常函数极限v al FU N C_CO N ST =h V 々. ( A x . 々)— 是.证明. 首先将目标中的全称量词去除, 然后用函数无穷极限的定理:F UNC_ PO S 对目标进行重写, 再分别使用定理:R EA L_SUB_R EFL 和ABS_0将目标中的“a bs U — 变为“0”. 此时的目标为:“ Ve .0 < e=>? X . V x . x >0 < e,,, 发现目标中的前件和结论都为“〇<e”, 那么就需要去除全称量词, 并使用策略DI SC H_TA C 将目标中的前件放在条件队列中, 最后用自动重写策略ASM _R EWRI T E_T AC □ 即可完成证明.证毕.( 6 ) 变量与常数之和的极限若函数/ 在正无穷远处存在极限, 即l i m/( x )=j - *4 - xL , 则有任意常数a 使得下式成立:l im/( a + x )= L.其形式化描述:定理8. 变量与常数之和的极限va lLIM_FU N C_LA M_AD D =I-V/ /+( 7 ) 变量与常数之积的极限若函数/在正无穷远处存在极限, 8 卩lim /Or )=L , 则有任意常数a >0 使得下式成立:l im /( a *x )=L.其形式化描述:定理9. 变量与常数之积的极限va lL IM_ FU NC_LA M_M UL =I-V // a . a ̄> 0A( A f . /< )-* ?/ (A f . / ( a *这两个定理通过消去全称量词, 并用函数无穷极限的定理对目标重写即可证明.4. 2 函数极限四则运算的建模与验证极限形式化语言只能证明极限, 不能求极限. 对于简单函数的极限问题, 可以使用比较容易的证明方法证明其极限存在或不存在, 但对于一些形式比较复杂的函数, 就不太容易证明. 因此, 函数正无穷极限的运算法则的形式化十分必要, 它对于证明复杂函数无穷极限的问题至关重要. 在上面正无穷极限的形式化模型的基础上, 这里将对正无穷极限的运算法则进行形式化建模及验证.在对函数在正无穷远处的极限的运算法则进行形式化描述和证明中, 形式化过程包括两种形式化内容.一种是在推出结果的形式中不带有而是使用“―” 的形式化, 这是最基本的形式化证明; 另外一种则是基于上一种证明的进一层, 是在推导结果中使用“=” 和Uim 的形式, 而这种形式是在后面函数极限的应用形式化建模中所需要的. 如若跳过第一层形式的证明, 直接到第二层, 则会有很多证明代码的冗余. 因此, 为了能够更加有效地组织这些证明逻辑、过程以及代码形式, 最终抽出第一层形成单独的定理形式, 这样在后续的证明过程中可减少不必要的重复证明.( 1 ) 函数极限加法若函数/ 和g 在正无穷远处都存在极限, 即l im /( x )= L , 则有函数/和 g的和在正无穷处存在极限并且:l im ( /( x ) + ^ ( x ) )= L +M.其形式化描述:定理1 0 . 函数加法val FU NC_A DD =I"^ f slt + gi l +m') .证明. 首先将全称量词去掉, 然后将t e nd S _r e al_r ea l 的定义进行重写, 去掉符号根据目标的形式使用MATC H 策略匹配定理N ET_AD D,目标会变成“d ord er¥>=”, 此时需要使用前面证赵春娜等: 函数极限的1 1 期 高阶逻辑形式 化建模与验证 2 1 25明过的定理2:D OR DER_RNGE 来说明“¥>=”满足有向集关系, 用MAT CH 接收策略将该定理代人即可.证毕.定理1 1 . 函数极限加法va l L IM_FUN C_AD D =I-V/ g/A g ̄>-m ^ (. i_l i m (.X x . f x+ g x )=Z + ?i ) .证明. 由于极限的运算是用f_ Hm 定义写的,所以首先去除全称量词及重写Ui m 的定义, 由于f_li m 定义中使用了选择操作运算符@ , 因此证明需要使用策略SE LECT _ELIM_ T A C , 这样就可以将目标转换为两个目标的合取形式,一个是证明存在性,一个证明等价性. 使用CO NJ _T AC 将目标中的合取形式变为两个子目标. 第一个子目标, 是证明两个函数的和在无穷远处存在极限, 根据前件中的条件函数/ 和g 在无穷远处的极限分别为Z 和因此只需要证明两个函数的和在正无穷远处的极限值为Z + m 即可. 那么就需要MAT CH _ MP_ T AC 对上面已经证明完的定理FU NC_ADD 进行匹配, 然后重写目标即可. 第二个子目标, 去掉全称量词后发现它的目标形式与之前证明函数极限的唯一性定理FUN C_ U NI Q 很相似? 此时需要使用M A TC H 策略匹配该定理, 则目标变成了“?乂xA i—G + m )” 的形式. 先证明目标合取式的第一部分, 即证明存在性, 显然存在的V 应该为( Ai. / x + g J: ) ,所以根据前件的条件可以消去目标合取式的第一部分; 而目标的第二部分与上面第一层证明极限和的形式一样, 所以使用MATC H 策略匹配定理FUN CLADD 即可.证毕.( 2 ) 函数极限减法若函数/ 和g 在正无穷远处都存在极限, 即l im /( x )= L , l i m 尽( _r )= M, 则有函数/ 和莒的X -*+ =C+CC差在正无穷处存在极限并且:l im+ o c其形式化描述:定理1 2. 函数减法v a lF UNC_SU B=Nfgl m. f一lt—g该定理的证明方法与定理1 0 是类似的.定理13 . 函数极限减法va l LIM_ F UN C_SU B=l—m ) .该定理的证明方法与定理1 1 是类似的.( 3 ) 函数极限乘法若函数/ 和g 在正无穷远处都存在极限, 即l i m /( x )= L , l im g ( x )= M, 则有函数/和g? 的X -*积在正无穷处存在极限并且:l i m ( / ( x )X ^( x ) )= L X M.J -* +OO其形式化描述:定理1 4 . 函数乘法va l F UN C_M UL =fglm . f—lt* gt l— U* m ) .定理I S . 函数极限乘法va l LIM_FU N C_MUL=卜V / gZm. /—Z A g—m => ( f_l im ( Ax. / x*g x )=l * m) .证明. 通过使用策略SELECT_E LIM _TAC ,可以将目标转换为两个目标的合取形式,一个是证明存在性,一个证明等价性. 使用CO NJ _TAC 将目标中的合取形式变为两个子目标. 第一个子目标, 是证明两个函数的乘积在无穷远处存在极限. 根据前件中的条件函数/ 和g 在无穷远处的极限分别为Z和?n , 因此只需要证明两个函数的和在正无穷远处的极限值为m X Z 即可. 那么就需要M A TCH _MP_TAC 对上面已经证明完的定理F UNC_MU L 进行匹配, 然后重写目标即可. 第二个子目标, 需要使用MAT CH 策略匹配该定理, 则目标变成了“?—x 八x'— 的形式, 先证明目标合取式的第一部分, 证明存在性, 显然存在的x' 应该为( A o r . / i*g x ) , 所以根据前件的条件可以消去目标合取式的第一部分; 目标的第二部分使用MATC H 策略匹配定理F U N C_MU L 即可证明.证毕.( 4 ) 函数极限与常数乘法若函数/ 在正无穷远处存在极限, 即l im/U )=L , 则有任意常数a , 使得a 与/ 的乘积在正无穷处存在极限并且:lim a X /( x )= a X L.其形式化描述:定理1 6 . 函数极限与常数乘法v al LIM_FU N C_CM UL=h V/ 1 a . f^ ̄l=>( f_l im (A x. a*f x )= a*V) : thm.证明. 由于该目标的形式与上一个定理: 函数极限的乘法运算很相似, 因此可以借助定理: LIM_2 1 2 6 计算机学报 2 0 2 0年FU NC_MU L 来进行证明. 那么就需要将目标的形式变成与所用定理一样的形式, 在定理LIM_ FUNC_M UL 中, 是两个函数乘积的形式, 而在证明目标中则是一个常数与一个函数的乘积形式, 因此需要使用定位策略及添加l am b da 函数的方法将常数改写为常函数的形式: CO NV _ TA C ( ( L A ND _CON V〇EXACT—CON V) [ X _ BETA_ CONV (—‘x : r ea l,--)(-‘a :r ea l’- -) ] ) . 应用到要证明的定理中, 则左侧即可表示为, 对目标中的常数a 添加一个自变量为?r 的l amb d a 函数. 此时的目标形式为:f_l im ( A x .( A x . a )〇: )= ? * /? 此时便可以使用M A TC H策略匹配定理LIM_ F UNC _MU L , 然后使用常函数极限定理FUN C _CO NST 进行重写, 即可完成证明.证毕.( 5 ) 函数极限除法若函数/ 和g 在正无穷远处都存在极限, 即l if/( x )= L , li iji g ( _r )= M, 并且M尹0 , 则有函k / 和g 的商i正无穷处存在极限并且:K( fU ) / g U) )= L /M.其形式i描述:定理1 7 . 函数极限除法va l FUN C_DIV =N fglh g— mi X t . ft/ g证明. 首先将全称量词去掉, 然后将t e nd S _re aLr e a l 的定义进行重写, 去掉符号“—”, 根据目标的形式使用MAT CH 策略匹配定理N ET_ DIV, 目标会变成“dor de r¥>=”, 此时需要使用前面证明过的定理2 : D 0R DER_RNG E 来说明“¥>=”满足有向集关系, 即用MATCH 接收策略将该定理代人即可.证毕.4 . 3 函数积分极限的高阶逻辑形式化建模与验证( 1 ) 正无穷函数积分上限取绝对值的建模与验证若函数/ 在以任意常数a 为积分下限存在正无穷积分L , 即l i mfV( x )= L , 则有该函数在以^j- * +<?J a为积分下限, 积分上限为取正无穷变量的绝对值的极限为L , 即p1l im/ ( x)= L .x -^ +〇〇J a该定理表示, 函数积分上限取极限时, 与其上限的绝对值取极限的结果一样. 其形式化描述如下:定理18 . 函数积分极限上限绝对值定理va l LIM_FUNC_BO UND_AB S =1- V/ a />.  ( A ^ . i nt e gral ( a , i )( A ? . i nt e gr a l( a ,a b sf )证明. 首先用极限定理FUNC_PO S 重写, 然后使用等价策略( EQ_ TAC ) 将等价性证明变换成两个蕴含式证明. 第一个子目标的蕴含式证明: 由于目标中存在两个蕴含式且它们之间的关系为蕴含关系, 每个蕴含式中都有一个〇所以先将两个e 实例化为同一个e , 主要使用SPEC , 即MP_ TAC〇 SPEC“e : re ar. 目标式中有存在量词的证明, 实际上在0< ? 时, a bs. 所以, 两个蕴含式中的X , 即存在量词, 可以写成一个? 此时, 目标变为“a b s ( i nt eg ral( a , a b sj: )而前件中有三个条件分别为“工X ”,“ Vx . _r> & X>a b s( i n te g ra l ( a , x )/—/>) <, 和“OO ”. 从条件2 中可以发现, 其成立的条件为“z >对目标来说, 它的成立条件形式应该为“abs& X”. 所以使用目标中的前件匹配结果, 即可得到目标: a bs : r > & X , 经过简单的变换, 根据条件即可完成第一个子目标的证明.第二个子目标的证明思路与第一个子目标很相似, 但第二个子目标中的蕴含式与第一个子目标中的蕴含式刚好相反, 条件和结果进行了调换, 所以在证明到目标形式为“a b s ( i nt eg ral ( a , :c ) / _p ) < e”的时候, 有所不同. 此时的前件条件中有“x > & X ”,MVo : . x > &- X =>a bs ( in t eg ra l ( a ,a bs x ) f ̄p') <i en和“0 < , . 此时条件2 中的目标中有“a b s的形式, 而条件中的前件却为并没有绝对值a b s 的形式. 而目标中也没有绝对值abs 的使用. 为了能使用前件中第二个条件, 需要将目标的形式改写为与前件第二个条件的目标相似的形式. 即用a b s i 代替目标中的X , 将目标变为“ab s ( i nt e gralU ,a b sz ) /_/> ) < ,. 而前件中第一个条件为“x > & X”,: c 为实数, 而X 为自然数, 因此会有“ & X” 的形式, 是将自然数取实数的表示方法. 由此可知, 若一个实数大于等于一个自然数, 那么这个实数与其绝对值是相等的.证明步骤如下:首先证明“〇< x”, 需要使用实数小于等于的传递定理REAL_LE_TRANS , 找到一个处于0 和x 的中间值, 那就是自然数兄于是分别证明“和“02 X”, 第一个目标用重写即可( 前件条件中有该目标的形式) . 第二个目标使用定理Z ER〇_ LESS_EQ ( 表示自然数不小于零) 即可证明.其次证明“x= ab sI”, 使用定理ABS_ REFL( 实

[返回]
上一篇:合成孔径雷达参数化成像技术进展_曾涛
下一篇:多尺度特征融合与特征通道关系校准的SAR图像船舶检测_周雪珂