Lebesgue积分在PVS中的证明分析
|
摘要
为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用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.
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.
引文
[1]AGUADO F,ASCARIZ P,CABALAR P,et al.Verification for ASP Denotational Semantics:A Case Study Using the PVS Theorem Prover[J].Logic Journal of the IGPL,2017,25(2):195-213.
[2]MASCI P,ZHANG Y,JONES P,et al.Formal Verification of Medical Device User Interfaces Using PVS[C]//International Conference on Fundamental Approaches to Software Engineering.Berlin:Springer,2014.
[3]LAWFORD M.Formal Translation of IEC 61131-3Function Block Diagrams to PVS with Nuclear Application[C]//NASA Formal Methods:8th International Symposium,NFM 2016.Minneapolis:Springer,2016.
[4]SOURI A,JAFARI N N.Behavioral Modeling and Formal Verification of a Resource Discovery Approach in Grid Computing[J].Expert Systems with Applications,2014,41(8):3831-3849.
[5]MYREEN M O,OWENS S.Proof-Producing Translation of Higher-Order Logic into Pure and Stateful ML[J].Journal of Functional Programming,2014,24(2/3):284-315.
[6]SKOGSRUD H,HEZHAD H,BENATALLAH B,et al.Modeling Trust Negotiation for Web Services[J].IEEE Computer,2013,42(2):54-61.
[7]MARISA T,NIEDERHAUSER T,HAEBERLIN A,et al.Pseudo Asynchronous Level Crossing ADC for ECG Signal Acquisition[J].IEEE Transactions on Biomedical Circuits and Systems,2017,11(2):267-278.
[8]王学彬.拉普拉斯变换方法解分数阶微分方程[J].西南师范大学学报(自然科学版),2016,41(7):7-12.
[9]王明华.函数向量Riemann边值逆问题[J].西南师范大学学报(自然科学版),2013,38(12):28-32.
[10]谷伟卿,施智平,关永,等.Gauge积分在HOL4中的形式化[J].计算机科学,2013,40(2):191-194.
[11]RIAZANOV A,VORONKOV A.The Design and Implementation of VAMPIRE[J].AI Communicaitons,2014,15(2):91-110.
[12]XU K,BOUSSEMART F,HEMERY F,et al.Random Constraint Satisfaction:Easy Generation of Hard(Satisfiable)Instances[J].Artificial Intelligence,2013,17(8):514-532.
[13]李黎明,关永,吴敏华,等.运用定理证明的形式化方法验证SpaceWire编码电路[J].小型微型计算机系统,2014,30(6):1372-1376.
[2]MASCI P,ZHANG Y,JONES P,et al.Formal Verification of Medical Device User Interfaces Using PVS[C]//International Conference on Fundamental Approaches to Software Engineering.Berlin:Springer,2014.
[3]LAWFORD M.Formal Translation of IEC 61131-3Function Block Diagrams to PVS with Nuclear Application[C]//NASA Formal Methods:8th International Symposium,NFM 2016.Minneapolis:Springer,2016.
[4]SOURI A,JAFARI N N.Behavioral Modeling and Formal Verification of a Resource Discovery Approach in Grid Computing[J].Expert Systems with Applications,2014,41(8):3831-3849.
[5]MYREEN M O,OWENS S.Proof-Producing Translation of Higher-Order Logic into Pure and Stateful ML[J].Journal of Functional Programming,2014,24(2/3):284-315.
[6]SKOGSRUD H,HEZHAD H,BENATALLAH B,et al.Modeling Trust Negotiation for Web Services[J].IEEE Computer,2013,42(2):54-61.
[7]MARISA T,NIEDERHAUSER T,HAEBERLIN A,et al.Pseudo Asynchronous Level Crossing ADC for ECG Signal Acquisition[J].IEEE Transactions on Biomedical Circuits and Systems,2017,11(2):267-278.
[8]王学彬.拉普拉斯变换方法解分数阶微分方程[J].西南师范大学学报(自然科学版),2016,41(7):7-12.
[9]王明华.函数向量Riemann边值逆问题[J].西南师范大学学报(自然科学版),2013,38(12):28-32.
[10]谷伟卿,施智平,关永,等.Gauge积分在HOL4中的形式化[J].计算机科学,2013,40(2):191-194.
[11]RIAZANOV A,VORONKOV A.The Design and Implementation of VAMPIRE[J].AI Communicaitons,2014,15(2):91-110.
[12]XU K,BOUSSEMART F,HEMERY F,et al.Random Constraint Satisfaction:Easy Generation of Hard(Satisfiable)Instances[J].Artificial Intelligence,2013,17(8):514-532.
[13]李黎明,关永,吴敏华,等.运用定理证明的形式化方法验证SpaceWire编码电路[J].小型微型计算机系统,2014,30(6):1372-1376.