【摘 要】
：
随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.
【机 构】
：
北京化工大学 信息科学与技术学院, 北京 100029;首都师范大学 信息工程学院, 北京 100048
论文部分内容阅读
随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.
其他文献
在Agent2D底层中,单一的防守和进攻方式往往不能很好的完成比赛所要求的进攻和防守任务.针对此问题,提出一种多人防守策略和三角进攻策略,多人防守策略是当对方处于进攻状态时,我方派出两名及以上队友去逼抢对方持球队员;三角进攻策略是通过合适位置的3名队友的跑位配合实现的,由一名核心进攻球员和两名辅助进攻球员组成三角进攻小组.将该策略应用到球队中,并在RoboCup仿真2D平台上进行实验.实验结果表明使用了多人防守策略和三角进攻策略的球队的胜率和防守进攻效率都得到了提升,验证了该策略有效性.
密码技术是云计算安全的基础,支持SR-IOV虚拟化的高性能密码卡适用于云密码机,可以为云计算环境提供虚拟化数据加密保护服务,满足安全需求.针对该类密码卡在云密码机使用过程中存在的兼容性不好、扩充性受限、迁移性差以及性价比低等问题,本文提出了基于I/O前后端模型的密码卡软件虚拟化方法,利用共享内存或者VIRTIO作为通信方式,通过设计密码卡前后端驱动或者服务程序,完成多虚拟机与宿主机的高效通信,实现常规密码卡被多虚拟机共享.该方法可以有效地降低云密码机的硬件门槛,具有兼容性好、性能高、易扩展等特点,在信创领
针对苏州市金鸡湖城市广场在突发情况下的人群疏散问题,建立了基于实时动态的疏散网络路径规划模型,分析了大型公众区域复杂环境对人群疏散效率的影响.同时提出以人群逃离危险区域的终止时间作为权值参数改进Dijkstra算法,并且利用反馈补偿机制合理分配各出口的疏散人数,实现人群疏散的动态调整和路径规划.通过Pathfinder软件仿真验证算法的有效性,得出改进以时间为权值的Dijkstra算法和提前规划人群疏散特定出口,可以获得更优的人群疏散结果,从而保障疏散人群的生命财产安全.
有效的刀具寿命预测可以提高加工效率,保证工件加工精度,因此具有重要的研究价值.刀具寿命预测受到刀具材质、切削参数以及加工材料等多因素的影响,导致刀具寿命难以准确预测.针对这一问题提出了一种利用粒子群(particle swarm optimization,PSO)算法优化径向基(radial basis function,RBF)神经网络的刀具寿命预测方法.首先用PSO算法优化RBF神经网络的主要参数中心值c,宽度σ以及连接权值w,然后将影响刀具寿命的多个因素作为PSO-RBF神经网络模型的输入神经元,寿
本文基于神经网络技术设计空调控制软件系统,对传统人工控制模式和神经网络控制器进行对比研究.首先利用Energy Plus仿真软件建立真实高铁站建筑及其多联机空调系统模型,对该空调系统设置424种工况完成了一整年运行仿真,然后从百万条仿真数据中抽取PMV(predicted mean vote,预测平均投票)热舒适度和能耗优秀的数据训练神经网络控制器,最后用JavaEE技术开发了该高铁站空调控制软件原型系统并利用Energy Plus仿真数据以及机器学习预测模型模拟实现了空调动态控制.实验结果表明,在冬季和
图结构数据是现实生活中广泛存在的一类数据形式.宏观上的互联网、知识图谱、社交网络数据,微观上的蛋白质、化合物分子等都可以用图结构来建模和表示.由于图结构数据的复杂性和异质性,对图结构数据的分析和处理一直是研究界的难点和重点.图神经网络(Graph Neural Network,GNN)是近年来出现的一种利用深度学习直接对图结构数据进行学习的框架,其优异的性能引起了学者高度的关注和深入的探索.通过在图中的节点和边上制定一定的策略,GNN将图结构数据转化为规范而标准的表示,并输入到多种不同的神经网络中进行训练
提出了一种基于条件生成对抗网络的情感语音生成技术,在引入情感条件的基础上,通过学习语音库中的情感信息,能够自主生成全新的富有指定情感的语音.生成式对抗网络是由一个判别网络和一个生成器组成.使用TensorFlow作为学习框架,利用条件GAN模型对大量情感语音进行训练,利用语音生成网络G和生成网络D构成动态“博弈过程”,更好地学习观测语音情感数据的条件分布.其生成样本接近原始学习内容的自然语音信号,具有多样性,而且能够逼近符合真实情感的语音数据.所提出的解决方案在交互式情绪二进制动作捕捉IEMOCAP语料库
基数估计是基于代价查询优化的关键步骤,已经被研究了近40年.传统方法如基于直方图的方法在一些假设如属性相互独立、相交的表满足包含原则等成立时能基本满足准确性要求.然而,在真实运行环境中这些假设往往不再成立,可能导致基数估计严重错误进而造成查询延迟.近年来,随着数据的增多和新硬件的发展,使用机器学习方法来提高基数估计的质量成为了可能.由于基于代价的查询优化主要根据查询中子执行计划的估计代价来选择最优的查询执行计划,因此,有一些最近的工作针对一些关键的子执行计划模板建立相应的局部学习模型,取得了不错的进展.但
如何准确高效地预测销量是企业一直以来关注的重要问题.传统的时间序列预测方法虽然在研究和实践中占主导地位,但是存在一定的局限性.随着大数据的发展,电商企业能获取前所未有的数据量和数据特征,仅利用过去的行为和趋势很难准确地对销量进行预测.本文提出一种基于随机森林、GBDT、XGBoost算法的成本厌恶偏向性组合预测模型,并利用每个商品的成本数据实现对样本的精细化赋权,进而输出预测结果.结果表明,组合预测模型能更精确预测销量,对电商企业降低商品管理成本有重要意义.
学生知识点熟练度是教师为学生制定学习计划的重要依据.为解决认知诊断中无法概率化学生知识点熟练度的问题,提出了将知识点作为特征嵌入的预测方法.该方法分别对学生和试题建立知识点向量,并且构造卷积神经网络进行监督学习,根据学生的答题情况不断调整他们的知识点熟练度.实验结果与现有的方法进行对比,验证了该方法的准确率的确有所提升.