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