基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

基于Coq的分块矩阵运算的形式化

矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结,并且分析了矩阵形式化的主要几种方法;其次介绍并...     

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型（RVWMO）规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理（加载值公理、原子公理与进度保证公理）描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。     

多旋翼飞控推进子系统的Coq形式化验证

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

基于Coq的矩阵代码生成技术

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

基于Coq的Paxos形式化建模与验证

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在定理证明工具Coq中,形式化描述和定义了Lamport的BasicPaxos算法,并且证明了其满足共识性.     

基于Coq构造携带证明的安全程序

对可靠程序的需求随着高可信软件在信息社会中的作用日益重要而增加。基于形式化证明工具构造携带证明的安全程序,给出严格的程序规范及其证明是提高软件可靠性的重要途径。论文介绍使用形式化证明工具Coq构造安全程序的过程和经验。     

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.     

Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators

The class of unquantified formulae of set theory involving Boolean operators, the powerset and singleton operators, and the equality and membership predicates is shown to have a solvable satisfiability problem.It is shown that whenever a formula in the above class is satisfiable there exists a hereditarily finite model of , whose rank is bounded by a doubly exponential expression in the number of variables occurring in .This paper was written while the author was a Visiting Professor at Courant Institute of Mathematical Sciences, New York University, U.S.A.     

集对分析的不确定性系统理论在AⅠ中的应用

根据不确定性与确定性对立统一的观点,把同一个研究对象相对于参考集的确定性测度与不确定性测度作为一个不确定性系统,用联系数描述这个系统,根据问题的要求对联系数作适当的运算,由此形成基于集对分析的不确定性系统理论.把该理论用于不确定性推理、智能计算、群体智能分析,思路清晰,算法简明,所得结果能较好地符合客观实际.     

集合论等式型定理机器证明系统的研究与开发

集合论定理机器证明,至今在国内外尚无相关研究。虽然集合论在数学领域中所处的基础地位显得在这一领域实现机械化极其重要,但是多年来尚无进展。到目前为止,还没有发现能产生可读证明的系统。通过对人工智能搜索算法的研究,提出了集合论等式型定理证明的机械化方法。实现的系统能自动生成定理的可读证明以及相关的说明。     

基于判别度的实值决策系统的属性约简

研究实值决策系统中的知识获取是粒计算研究的主要方向之一。为给出一种高效的知识获取方法,基于邻域粗糙集的原理,针对实值特点,在相容的实值决策系统中,给出判别度描述下的约简定义。进一步提出一种基于判别度的属性约简的启发式算法,同时对算法的性质进行了分析,通过实例验证了算法的有效性。     

公理化模糊共享近邻自适应谱聚类算法

针对传统的谱聚类算法通常利用高斯核函数作为相似性度量,且单纯以距离决定相似性不能充分表现原始数据中固有的模糊性、不确定性和复杂性,导致聚类性能降低的问题。提出了一种公理化模糊共享近邻自适应谱聚类算法,首先结合公理化模糊集理论提出了一种模糊相似性度量方法,利用识别特征来衡量更合适的数据成对相似性,然后采用共享近邻的方法发现密集区域样本点分布的结构和密度信息,并且根据每个点所处领域的稠密程度自动调节参数σ,从而生成更强大的亲和矩阵,进一步提高聚类准确率。实验表明,相较于距离谱聚类、自适应谱聚类、模糊聚类方法和地标点谱聚类,所提算法有着更好的聚类性能。     

集对分析的不确定性系统理论在AI中的应用

根据不确定性与确定性对立统一的观点，把同一个研究对象相对于参考集的确定性测度与不确定性测度作为一个不确定性系统，用联系数描述这个系统，根据问题的要求对联系数作适当的运算，由此形成基于集对分析的不确定性系统理论．把该理论用于不确定性推理、智能计算、群体智能分析，思路清晰，算法简明，所得结果能较好地符合客观实际．     

基于集对分析联系数故障树的BA系统可靠性分析*

为了有效管理和监测建筑设备自动化系统（BAS）,提高系统可靠性,基于集对分析联系数和故障树理论研究了BA系统的可靠性分析方法。详细分析可能引起BA系统故障的各种因素,建立系统的故障树模型,并确定了系统故障原因的各种可能组合方式;引入中间状态概率的概念结合集对分析联系数理论建立了BA系统的可靠性评定模型;通过BA冷源系统的仿真实例验证了模型的可靠性和有效性。实验表明,该模型便于发现系统的薄弱环节,从而有效提高了系统的可靠性。     

统一集论在病体供应链建模中的应用

供应链系统是一复杂巨系统,它的结构和运作模式决定了其复杂性。文章从认知思维基础出发来认识供应链系统的复杂性并将智能数学的最新成果——统一集及其分支运用于供应链系统的建模。     

基于粗集理论的证据加权组合方法及其应用

对于证据理论中不同来源的证据具有不同的重要性,在信息融合过程中,若能把不同重要性的证据准确表达出来就可以提高融合精度.为此,提出了一种基于粗集理论的加权证据多源信息融合方法,在证据理论中引入证据权的概念,根据粗集理论和证据理论的基本关系,利用粗集理论进行不同信息源证据权的发现.应用柴油机状态评估实例进行验证,研究表明,该方法避免了传统证据理论的主观因素影响,能有效提高融合结果的准确性,并且融合过程更有逻辑性.