摘要
为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用Lebesgue积分的运算特征在PVS定理证明器中进行形式化证明与分析.主要对其分裂定理、不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则和极限定理等多个方面进行了形式化,且依据数学定理与推论形式化,说明Lebesgue积分在PVS中的形式化是可行的、有效的.以标准反相积分器为应用模型,对其通用电路原理与机制进行了形式化证明,通过数理分析测试了本文Lebesgue积分形式化定理库的正确性.
In order to solve the formal problem of verification and test theorem of function system modeling,signal real-time analysis supported by mathematical domain,we design and implement the formal proof and analysis of the Lebesgue integral in PVS theorem prover.This paper formalized the operational the properties of integration,and include the split theorem,inequality calculations,and integrability on a subinterval,multiple segments,linear operation,Cauchy-type integrability and limit theorem criterion of lebesgue integral in PVS.And according to the mathematical theorem and inference formalization,which shows that Lebesgue integral in PVS formalization is feasible and effective.The principle and mechanism of the general circuit are proved by using the standard inverting integrator as the application model.The correctness of the Lebesgue integral formal theorem is proved by mathematical analysis.
作者
王彩
高晓琴
WANG Cai;GAO Xiao-qin(Department of Computer Science and Technology,Chengdu Neusoft University,Dujiangyan Sichuan 611844,China;Department of Information Engineering,Sichuan Technology&Business College,Dujiangyan Sichuan 611837,China)
出处
《西南师范大学学报（自然科学版）》
CAS
北大核心
2018年第1期61-69,共9页
Journal of Southwest China Normal University(Natural Science Edition)
关键词
LEBESGUE积分
PVS
形式化证明
反相积分器
Lebesgue integral
PVS(Prototype Verification System)
formal proof
inverting integrator
