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