函数极限的高阶逻辑形式化建模与验证  

Formal Modeling and Verification of Function Limit in Higher-Order Logic

作　　者：赵春娜 赵刚 ZHAO Chun-Na;ZHAO Gang(School of Information Science and Engineering,Yunnan University,Kunming 650500)

机构地区：[1]云南大学信息学院,昆明650500

出　　处：《计算机学报》2020年第11期2119-2133,共15页Chinese Journal of Computers

基　　金：国家自然科学基金(61862062,61104035)资助.

摘　　要：在高阶逻辑定理证明器中研究了函数无穷远处极限的形式化建模和验证,包括函数无穷远处极限定义的形式化模型,函数极限相关性质的建模与验证,有唯一性、保不等式性、绝对值函数在无穷远处的极限、极限等价性、常函数极限等.函数无穷远处极限的高阶逻辑定义是利用拓扑极限方式定义的,并在实数域内利用集合关系等验证定理.根据集合有序关系定理验证了唯一性.利用差值和绝对值的高阶逻辑性质验证极限为零的属性.变量与常数之和与积的极限高阶逻辑定理也通过已验证定理和高阶逻辑策略验证了.建立了函数极限四则运算的高阶逻辑模型,并验证了函数极限加法、函数极限减法、函数极限乘法、函数极限与常数乘法、函数极限除法的高阶逻辑定理.也建立了函数积分极限的高阶逻辑形式化模型,验证了函数积分极限上限绝对值定理、函数积分极限上限可加定理、函数积分极限上限可乘定理.在此基础上,建立了拉普拉斯变换卷积定理的高阶逻辑形式化建模与验证.最后,对电阻-电感电路中的电流进行了高阶逻辑形式化建模与验证,建立了单位阶跃信号和电路中电流的高阶逻辑形式化定义,并验证了其正确性.该实例验证表明了函数极限和相关性质的高阶逻辑形式化模型的正确性,为后续控制系统的形式化分析奠定了良好的基础.Function limit of infinity is studied in higher order logic theorem prover in this paper.Formal modeling and verification of function limit are created in higher order logic.Higher order logic model of function limit plays a significant role in the formalization of fractional order systems.Firstly,based on higher order logic models of set and number,formal model of function limit definition and its related properties are proposed in this paper.These attributes include the basic nature of function limit—uniqueness,inequality preserving property,the absolute value function limit when solving its positive infinity limit,limit equivalence,constant function limit,etc.Higher order logic definition of function limit is defined by topological limit way.Then higher order logic theorem is verified based on sets and relations in the real domain.The uniqueness theorem is validated on account of the sets the orderly relations theorem.The inequality preserving property is verified through the higher order logic validation strategy.The zero limit theorem is tested by higher order logic properties of difference and absolute value.The limit equivalence and constant function limit theorems are verified in higher order logic.The limit of the sum of variable and constant and the limit of the product of variable and constant also are validated based on the higher order logic validation strategy and the verified theorems.Higher order logic model of arithmetic of function limit is also established in higher order logic theorem prover.And some related theorems are verified.The function limit addition higher order logic axiom is validated on the basis of higher order logic model of function addition.The function limit subtraction higher order logic proposition is verified on the grounds of higher order logic model of function subtraction.The function limit multiplication higher order logic theorem is validated in the light of higher order logic model of function multiplication.Then higher order logic theorems of multiplication of funct

关 键 词：函数极限 高阶逻辑 形式化验证 定理证明 卷积 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]