定理证明

摘要： 区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群机器人工作场景的高阶逻辑表达;完成了机器人移动概率和平均移动概率的建模与验证;最终验证了一定时间步长内群机器人在特定区域内的覆盖率的正确性.为实现多种复杂场景下群机器人区域覆盖算法的高阶逻辑定理证明形式化分析奠定基础.

摘要： 以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。

摘要： 矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.

摘要： 飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

摘要： 为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

摘要： 定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

摘要： 随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.

摘要： 对斯坦纳-莱莫定理的历史作简要回顾,给出一般性的推广,并研究了它的若干等价形式.通过构造函数而给出一种新的证明(包括一般形式的).

摘要： 初中阶段数学素养主要表现为抽象能力、运算能力、几何直观、空间观念、推理能力、数据观念、模型观念、应用意识、创新意识.推理能力是其重要组成部分.在初中数学教学中,数学定理的教学重在培养学生数学逻辑推理能力.教师应在探究命题的各个环节中设计合理的教学程序,提出有思维价值的问题,促使学生深度学习,培养学生的数学推理能力.

摘要： 例题教学是深化知识理解、提高解题思维、发展核心素养的重要方式。要发挥例题的深层教学价值,教师需要深入思考,把握例题教学方向;巧妙设计问题,驱动学生积极参与,从而实现由“怎样做”到“怎样想”,提高解题水平。

摘要： 指出了目前国内外不少《大学物理》教材中有关刚体平行轴定理证明对普遍存在的一些错误和概念的混淆,并进行了分析和澄清.

摘要： 形式化软件方法采用数学的方法对软件进行建模和验证,可提高软件安全性.本章讨论了软件的形式化开发方法,讨论了形式化验证的问题,重点关注了论了定理证明和模型检验的局限性,综述了当前降低模型检验开销的研究进展.

摘要： 目前,粗糙集理论存在着两种观点,它们分别是代数观和信息观.在代数现点中,知识粗糙性体现了知识的粒度;而在信息观中,定义了知识的信息熵和条件信息熵.已经有定理证明了信息熵与知识的粗糙性存在对应关系,它建立了代数观和信息观之间的联系,但是这种关系却不是一一对应的.该文通过重新证明知识粗糙性和信息熵的对应关系定理,找到与知识粗糙性存在一一对应关系的是条件信息熵,并给出相关定理及其证明.

摘要： 本文用Paulson归纳法描述并发系统,对系统执行的不确定性进行建模,给出了一种适合定义测度的产生集合,利用测度评估函数将产生集合的测度与有限执行序列的测度联系起来;证明执行序列集合上的测度满足非负性和可列可加性,利用测度扩张定理构造并发系统执行序列集合上的概率空间.所有证明脚本经过定理证明工具Isabelle/HOL/Isar的检查.

摘要： 基于Tableau方法的z规格说明求精以定理证明为基础,将从规格说明得到程序的过程看作是一个定理证明的过程,如果这个证明存在,那么从证明中可抽取出一个满足该程序规格说明的程序.本文引进合并规则扩充Tableau方法的演绎规则,并利用该规则给出了Z语言中模式的与、或操作的求精方法,从而简化了模式复合的求精;为了使Tableau方法能够用于Z规格说明的求精,我们将Z语言的结构成分转化为Tableau方法所能接受的结构.

摘要： 基于Tableau方法的程序综合方法以定理证明为基础,将从规格说明得到程序的过程看作是一个定理证明的过程,如果这个证明存在,那么从证明中可抽取出一个满足该程序规格说明的程序.本文证明了通过程序综合方法构造得到的程序是完全正确的程序.

摘要： 在Goetschel-Voxman所引进的序关系下,首先给出了生成函数的概念,证明了由一类凸集生成的函数是模糊值凸函数;其次利用上图的性质,建立了模糊值凸函数的下卷积、右乘等概念,并给出了相应的定理;最后讨论了模糊值函数的凸化问题,并给出了其刻画定理.

摘要： 在Goetschel-Voxman所引进的序关系下,首先给出了生成函数的概念,证明了由一类凸集生成的函数是模糊值凸函数;其次利用上图的性质,建立了模糊值凸函数的下卷积、右乘等概念,并给出了相应的定理;最后讨论了模糊值函数的凸化问题,并给出了其刻画定理.

摘要： 在Goetschel-Voxman所引进的序关系下,首先给出了生成函数的概念,证明了由一类凸集生成的函数是模糊值凸函数;其次利用上图的性质,建立了模糊值凸函数的下卷积、右乘等概念,并给出了相应的定理;最后讨论了模糊值函数的凸化问题,并给出了其刻画定理.

摘要： 安全协议形式化分析与验证技术是计算机网络安全领域的重大课题之一。形式化方法多种多样。文中首先描述了形式化分析的前提,然后采用对比的方式详细介绍了目前流行的几种形式化验证技术的验证过程及相应的优缺点,并介绍了一种新的验证技术-类型检测方法,最后指出目前在这方面所做的工作以及未来的发展方向。

摘要： 本发明属于密码学隐私保护领域，公开了一种基于拉格朗日三整数定理和内积的大小恒定的零知识范围证明方法，具体步骤包括：步骤1：生成公共参数；步骤2：生成秘密值和承诺值；步骤3：证明者将这些承诺值发送给验证者；步骤4：验证者向证明者发送挑战值；步骤5：证明者第一次生成回复值并发送给验证者；步骤6：验证者第二次向证明者发送挑战值；步骤7：证明者第二次生成回复值并发送给验证者；步骤8：验证者验证等式是否成立。本发明与其它方案相比，有更快的速度与更低的存储开销，并且无论的范围有多大，该方案所需要消耗的时间以及证明数据的大小都在一个常量范围内。

摘要： 本实用新型公开了容积转换式勾股定理快速简易证明装置，由平面板和内腔为直角三角形的管体构成，内腔为直角三角形的管体横断面内腔为直角三角形，其特征在于：所述的内腔为直角三角形的管体的底端口为封膜平口，置于平面板的板面上，内腔为直角三角形的管体的上端口的两个直角边板的高度分别与直角三角形的勾、股边长度一致，分别组成勾、股边正方形板；内腔为直角三角形管体的上端口第三个边板的高度与直角三角形的弦边长度一致，组成弦边正方形板；勾边正方形板、股边正方形板和弦边正方形板均设有夹层腔。该容积转换式勾股定理快速简易证明装置，结构简单、操作步骤少而方便，通过测量容量的方式，快速、明了、形象的证明了勾股定理。

摘要： 本发明提出一种基于HybridUML和定理证明的CPS自适应性验证方法，主要用于解决形式化验证方法理论性过强所带来的难以普遍应用的难题。本发明步骤包括：首先利用HybridUML视图对CPS建模；然后将HybridUML规约转换为定理证明器KeYmaera的输入-量化混合程序QHP；结合生成的QHP，以量化微分动态逻辑QdL公式的形式对待验证的属性进行规约，然后利用KeYmaera进行自动验证；进行模型转换之前，需要定义HybridUML和QHP的元模型，转换时首先消除顶层Mode具有的层次性，转换后得到的模型称为FlatMode，然后根据FlatMode和QHP之间宏观语义以及元语义的一致性确定转换规则，然后利用ATL语言描述转换规则，实现FlatMode模型到QHP媒介模型的转换，然后利用自定义模板语言实现QHP媒介模型到QHP代码的转换。

摘要： 本发明涉及一种基于PVS的PPTLI定理证明的形式化验证方法，包括：S101：通过PVS构建得到PPTLI的基本时序类型和PPTLI的索引表达式类型，并根据PPTLI的索引表达式类型等价表示线性时序逻辑；S102：根据PPTLI的基本时序类型和PPTLI的索引表达式类型，通过PVS构建得到PPTLI定理证明系统；S103：将待证明的PPTLI时序性质表示为定理，利用PVS交互式证明命令使用PPTLI定理证明系统对待证明的PPTLI时序性质进行证明。本发明的方法借助于PPTLI这种表达能力强且综合统一的时序逻辑来描述和证明计算机系统预期的性质，能够弥补现有定理证明技术的不足，以保障系统的安全性和可靠性。

摘要： 本发明公开了一种基于冲突演绎的自动定理证明方法、装置及存储介质，在满足冲突演绎条件时，基于一阶逻辑子句集S获取虚子句、单元子句集及候选子句构建演绎子句集Q，对Q进行矛盾体分离并得到分离式R；当R为空子句时，冲突分析得到学习子句，在学习子句为空子句时定理被证明；否则，当R为单元子句且满足限定条件时，根据R在S中选取演绎子句加入到Q中，在Q中继续选择子句进行演绎；当R为非单元子句或不满足限定条件时，回退到上一演绎步骤，在Q中重新选择子句进行演绎。通过本发明的实施，灵活选取不同虚子句以简化演绎分离式，可有效缩减多元演绎的路径搜索空间和提升演绎效率，增强了多元演绎推理系统的一阶逻辑自动定理证明能力。

摘要： 本发明公开了一种基于超演绎的自动定理证明方法、装置及存储介质，从一阶逻辑子句集S选择包括单个核子子句及多个电子子句的子集构建标准矛盾体，得到矛盾体分离式R。若R为空子句，定理被证明。当R不为空子句时，若R有效且全为正文字，则将R加入到S中，停止本次矛盾体分离超演绎；当R含负文字，则在S中重新选择子句继续演绎；若无效，需回退到上一演绎步骤，在S中重新选择子句继续演绎；当S遍历完或满足定理判定终止条件，结束本次矛盾体分离超演绎。通过本发明的实施，具有每个矛盾体分离演绎只有1个子句含负文字的特点，能有效缩减多元演绎的路径搜索空间和提升演绎效率，增强了多元演绎推理系统的一阶逻辑自动定理证明能力。

摘要： 本发明公开了一种基于单元结果演绎的自动定理证明方法、装置及存储介质，对于一阶逻辑子句集S选择单元子句C，根据C在S中选择演绎子句集Q，采用C、S中剩余单元子句组成的单元子句集V以及Q中选择的子句构建矛盾体分离式R；若R为空子句，则定理被证明；若R有效且为单元子句，则将R加入到S中，在Q中重新选择子句继续演绎，当Q遍历完，在S中选择其它子句继续演绎，当S遍历完或满足演绎终止条件，结束本次矛盾体分离单元结果演绎。通过本发明的实施，矛盾体分离单元结果演绎充分发挥了多个子句之间的协同关系，能有效缩减多元演绎的路径搜索空间和提升演绎效率，增强了多元演绎推理系统的一阶逻辑自动定理证明能力。

摘要： 本发明公开一种基于定理证明的形式化验证方法，应用于安全操作系统领域，针对现有的操作系统存在的安全性问题，本发明基于定理证明的形式化验证方法，包括：对源代码重构、对函数进行形式化建模、对函数进行定理描述、最后进行形式化证明；本发明采用人机交互的半自动化证明，利用类型系统和逻辑之间的同构关系，将构造证明的过程转化为编写程序的过程，而证明的正确性检查也变成了类型检查问题，尽管需要大量手工劳动来构造证明，但是本发明提出的方法无需牺牲规约和代码的表达能力，特别是程序中可以使用表达能力很强的逻辑来表示，且证明自身在机器中都有显示表示，其正确性可以被自动检查，验证的结论也就更加可信。

摘要： 本发明公开了一种基于抽象语法树和定理证明的局部敏感程序分析方法，包括：对程序代码构建出没有语法错误的抽象语法树AST；遍历程序代码的抽象语法树AST，收集待检测节点及待检测节点的相关节点，根据待检测节点及其相关节点信息，形成待检测节点的相关逻辑表达式，输入至定理证明器中；定理证明器通过逻辑表达式求解待检测节点，若求解获得的待检测节点值存在异常情况，则判定程序存在语义缺陷。本发明通过收集程序节点局部上下文和局部路径信息，避免某些错误的报警以及提高易用性，实现了对程序代码的语义缺陷检测，避免了传统的符号执行工具分析代码因为路径爆炸问题而耗时长的问题。

摘要： 本公开实施例公开了一种基于机器学习的定理证明方法、装置、电子设备及存储介质，所述基于机器学习的定理证明方法包括根据目标命题获取所述目标命题的中间推理步骤；利用预先训练好的识别模型从所述中间推理步骤中确定能够用于证明所述目标命题的目标推理步骤；通过形式化定理证明方式利用所述目标推理步骤证明所述目标命题。该技术方案简化了目标命题的证明过程，压缩了中间推理步骤的搜索空间，提高了命题证明的效率及自动化程度。