【摘 要】
：
为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用Lebesgue积分的运算特征在PVS定理证明器中进行形式化证明与分析.
【机 构】
：
成都东软学院计算机科学与技术系,四川工商职业技术学院信息工程系
论文部分内容阅读
为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用Lebesgue积分的运算特征在PVS定理证明器中进行形式化证明与分析.主要对其分裂定理、不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则和极限定理等多个方面进行了形式化,且依据数学定理与推论形式化,说明Lebesgue积分在PVS中的形式化是可行的、有效的.以标准反相积分器为应用模型,对其通用电路原理与机制进行了形式化证明,通过数理分析测试了本文Lebesgue积分形式化定理库的正确性.
其他文献
梯田是山区提高农业综合生产能力、防止水土流失、改善生产生活条件的重要途径,地处黄土高原地区的隆德县50多年来的梯田建设印证了梯田建设的重要性和它发挥的作用。本文以
中国五四时期的文学恰好与日本近代文学处于同一个时间节点。这一时期,日本近代文学的自然主义理论在日本文坛中占有重要位置,对五四时期中国文学的影响最大。以浅析日本文学
散文是最贴近日常生活和日常表达的文类,其中,闲话絮语式的小品文尤其如此。现代散文从传统散文"载道"的模式中脱离开来,对日常生活敞开。然而,如何超越日常生活,做到言近旨
宁夏彭阳县建县以来狠抓机修梯田建设,梯田面积已达到4.4万hm2,人均新增机修梯田面积0.17hm2。总结出机修梯田建设的成果与效益、施工的质量与验收管理、设计及机修梯田时应
随着全球一体化的进程,项目管理在各行各业的建设中发挥出了巨大的功效。在项目建设过程中,一旦对于项目中的组织、进度、质量、成本等环节缺失了管理,将导致项目建设产生巨
大数据时代,海量资源给用户快速从浩瀚的资源中获取所需信息带来了难题,个性化推荐系统的市场需求越来越大。案例推理技术在个性化推荐系统中的应用还很少,因此,提出了基于案
绩效管理与企业文化融合是复杂多变的市场竞争形势和生产力快速发展的需要,其实质是充分发挥二者合力作用,达到事半功倍的效果。本文在系统阐述绩效管理与企业文化基本理论及
无形资产是经济发展的重要“驱动力”,已经成为体现企业创新和可持续发展能力的重要资产。上市公司无形资产数量和质量被视为核心竞争力的标志,尤其是专利权等知识产权,关乎