一、关于自然数集合上的递归定理（论文文献综述）
李亚男[1]（2020）在《基于Coq的Paxos的形式化建模与验证》文中进行了进一步梳理随着互联网的迅速发展和普及,网络数据流量越来愈庞大。企业信息化程度的不断加强,导致大量的数据亟待处理,数据已成为各类企业的命脉。传统的应用服务使用单一服务器模式,但是由于网络环境的不稳定,服务器容易发生数据丢失、节点宕机,严重影响了系统的可用性。在单机服务逐渐不能满足企业数据处理的需求情况下,人们开始搭建服务器集群的分布式系统。副本复制技术提高分布式系统的可靠性,在网络负载较大的情况下实现负载均衡,缓解服务器的压力。但是副本复制技术的引入,也带来了副本数据一致性等问题。为了保证系统的高可用性和一致性,就需要使用分布式一致性算法,Paxos算法便是其中非常重要的一类。共识问题是指分布式系统中一组参与者就一个结果达成一致的过程。Paxos能够很好的解决共识问题,越来越多的研究者将重点放在对算法本身的优化或者具体工程实现,Paxos在大型分布式系统得到了广泛的运用,比如区块链系统以及谷歌文件系统等。虽然Paxos的工程实现越来越多,但是关于算法安全性的形式化工作却很少,为了增强研究者和企业对Paxos的应用信息,其安全性证明越来越重要。所以,本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法。Paxos是应用在非拜占庭容错模型下的基于异步通信网络的分布式一致性算法。消息可能会延迟、丢失、顺序错乱,系统节点可能会发生故障,也可以重启;但是系统中不会出现恶意节点。利用这些性质,我们设置全局消息通道来解决在异步网络中定义节点的发送与接收消息的困难;同时,Paxos的消息种类非常复杂,我们利用Coq类型检查机制完成了消息类型的统一;最后,因为Paxos算法流程涉及到系统节点的过往信息,为了避免函数递归出现栈溢出等异常情况,我们增加了这些过往信息字段的定义,并对其及时更新,以此解决了复杂计算问题。我们选取了任意系统时间点,证明了其满足共识性,从而完成了对Paxos的形式化验证。
范一凡[2]（2020）在《基于Coq的“模”观点下线性代数机器证明系统 ——特例：模分解定理的机器证明》文中研究表明近年来人工智能发展迅速,已经上升为国家级重大战略,夯实人工智能的基础理论尤为重要。数学定理的机器证明是人工智能基础理论研究的深刻体现,是计算机科学和数学的完美结合,其主要通过计算机对数学理论进行形式化描述并验证定理证明的正确性。随着Coq、Isabella、HOL Light等证明辅助工具的出现,定理的机器证明取得了长足的进展。法国布尔巴基学派认为现代数学由序、代数、拓扑三大母结构组成。线性代数在各种代数分支中占据首要地位,线性代数中仅仅讨论向量空间的结构性质是片面的,还要考虑线性变换在其上的作用,这正是模观点的独到之处。用近世代数中的模理论来研究线性代数,使得线性代数从古典走向现代,带有线性变换的向量空间可以看做主理想整环上的模,因此模分解定理对向量空间的分解具有重要作用。本文基于证明辅助工具Coq,从本实验室的科研成果——“公理化集合论”形式化系统出发,初步实现了模观点下线性代数系统的形式化,并在此基础上完成了模分解定理的机器证明。主要工作如下:1、利用Coq,以“公理化集合论”形式化系统为基础,龚升的《线性代数五讲》为理论依据,形式化构建了群、环、体、域、主理想整环等代数结构,并完成了主理想整环上素元分解定理的机器证明。2、实现了向量空间和模两种代数结构的形式化,并用代码阐述了两者主要的联系与区别。至此,初步建立了代数结构的形式化框架。3、完成了主理想整环上有限生成模分解定理的机器证明,包括有限生成模分解定理的机器证明、准素唯一分解定理的机器证明和循环分解唯一性定理的机器证明。此定理可看做是向量空间与模之间的桥梁,这对线性代数后续的形式化研究意义重大。本文所有形式化过程已被Coq验证,体现了基于Coq的数学定理机器证明具有可靠性和严谨性的特点,证明过程规范、可读、智能。
盛枫[3]（2019）在《基于定理证明器Coq的形式语义验证研究》文中研究说明随着现代计算机系统的规模越来越大、复杂性越来越高,如何开发可信的软硬件系统已经成为计算机科学发展的巨大挑战。形式化方法是以数学理论为基础,对计算机系统进行严格地规约、建模与验证,实现系统的可信验证。形式化方法已经成为软件开发过程中不可或缺的一个环节,如何使用交互式的定理证明器对软件系统进行机械定义与验证是其中的一个研究重点。通过机械证明模型中的定理可以找出模型中存在的问题和漏洞,从而进一步提高模型的可靠性。本文的工作致力于研究软件开发过程中不同层次的形式语义验证,以代码层面的多线程离散事件仿真语言和系统建模层面的统一建模语言为研究对象,提出了将基于定理证明器Coq的机械验证引入到形式语义验证的研究中,使得基于Coq的机械验证涵盖整个软件开发生命周期。多线程离散事件仿真语言MDESL是一种类似于Verilog的底层硬件描述语言,在定理证明器Coq中实现了从MDESL代数语义中机械生成操作语义的过程,并且机械验证了生成操作语义的正确性和完备性。基于程序统一理论（UTP）,使用Coq中的高阶逻辑特性对MDESL的指称语义进行机械刻画,对代数定律的正确性进行机械验证。统一建模语言UML是一种通用的建模语言,在定理证明器Coq中实现了UML类图的机械语义。基于机械语义,在Coq中机械刻画类图的精化关系和静态模型的一致性,并提出了基于定理证明器Coq的可机械验证的UML模型框架。本文的主要内容和贡献包括如下几点:·提出了在定理证明器Coq中刻画从MDESL代数语义机械生成操作语义的过程,同时机械验证了生成的操作语义的正确性和完备性。根据代数语义,程序可以表示为具有位置状态的卫兵选择。在首规范型的基础上,定义了操作语义的生成策略,从代数语义生成的操作语义以定理的形式表示。使用Coq中的归纳类型、函数和归纳谓词来表示卫兵选择、首规范型和生成策略,使用Coq中的定理表示生成的操作语义,利用Coq的高阶逻辑证明系统对生成的操作语义的正确性和完备性进行机械验证。本文使用机械化的方法实现了原本只用手工证明的MDESL语义连接理论。·开展了在Coq中对MDESL指称语义的机械定义和代数定律正确性的机械验证研究。根据程序统一理论,基于观察的MDESL指称语义可以使用离散时间语义模型和健康公式来表示。使用Coq中的关系谓词和高阶逻辑来表示观察、健康公式和指称语义,在Coq中以定理的形式实现对代数定律的机械定义,并机械验证了代数定律的正确性,从而揭示了指称语义的正确性。本文创新性地实现了MDESL代数定律正确性的机械验证,利用Coq的高阶逻辑证明系统,降低了证明的难度,简化了证明的过程,推动了UTP理论的工程化发展。·研究了在定理证明器Coq中实现UML静态模型的机械语义,并对类图的精化关系和静态模型的一致性进行机械验证。使用Coq中的归纳类型定义UML静态模型,使用谓词逻辑刻画类图的良构规则与精化规则,利用Coq的证明系统对精化规则和静态模型的一致性进行验证。在此基础上,提出了基于定理证明器Coq的可验证UML模型框架,通过自动转换算法与工具的协助,对UML的形式语义机械化,为模型驱动的软件开发方法的形式验证提供了理论基础,为系统的可靠性提供支持。
唐大钊[4]（2019）在《限制分拆的算术性质和Catalan数的研究》文中研究说明自18世纪数学家欧拉所处的时代以来,人们对整数分拆理论的研究一直热情不减。该理论作为一个自成一体的独立数学分支,被不断发现它在其他数学分支中的应用,而包括Ramanujan同余式在内的着名结果又让它充满了传奇色彩。Catalan数可能是数学中无处不在的数字序列,Catalan数在组合数学,数论,代数,分析,几何,拓扑等领域有很多应用。关于经典Catalan数的推广不胜枚举。本文的主要研究对象为两类限制分拆,即2-着色分拆三元组和k-着色分拆,以及一类（7）q,t（8）-Catalan数。对于这两类限制分拆函数,我们得到了许多Ramanujan类型的同余式。对于k-着色分拆数,我们另外得到一些不等式。此外,利用禁模式排列,我们给出这类（7）q,t（8）-Catalan数若干种新的组合解释及其对应的gamma分解。本文主要分为以下七个章节:第一章,绪论。主要介绍数学背景,以及整数分拆和Catalan数的相关进展。另外,我们简要的描述本文各章的主要内容。第二章,对于分拆函数p3,1（n）,p3,3（n）,和p3,9（n）,我们分别得到了若干组无穷族模3幂次的同余式。另外,我们得到了两组关于p5,1（n）模5的同余式和三组关于p25,1（n）模5幂次的同余式。这里,kp,3（n）计数所有n的2-着色分拆三元组的个数,其中一种颜色只能出现在k倍数的分拆部分上。第三章,对于k-着色分拆函数p-k（n）,我们利用初等方法得到了一些模25的无穷族同余式。进一步地,对于k（28）2,6,和7,我们证明了很多Ramanujan模5幂次类型的同余式。第四章,受到Bessenrodt和Ono关于普通分拆函数的一个不等式的启发,对所有的整数k?2,我们得到了关于k-着色分拆函数p-k（n）的一些不等式。第五章,对于k-着色分拆函数p-k（n）,我们引入了一个广义奇异秩（k-奇异秩）。受到Andrews和Lewis以及Ji和Zhao工作的启发,我们得到了这种新定义的k-奇异秩的两个结果:我们首先对m（28）2,3,和4的情况得到了涉及Mk（7）r,m,n（8）的若干不等式;我们接下来对k（28）2和3的情况证明了偶数加权对称k-奇异秩矩的符号交错性。最后,我们提出了一个涉及Mk（7）m,n（8）的单峰性猜想。第六章,我们首先利用禁模式排列给出了一类（7）q,t（8）-Catalan数的若干新组合解释以及其对应的gamma分解。另一方面,对每个禁一个长度为3的模式的排列集合,我们得到了定义在上述集合上的（7）-1（8）-现象的一个完全刻画。利用这些新的gamma分解以及Shin和Zeng的一个五变元生成函数的连分式,我们进一步得到这些（7）-1（8）-现象对应的q-模拟。第七章,在本章我们主要对本文的工作进行一个梳理和总结,并且提出后续进一步研究的内容。
孔祥雯[5]（2019）在《基于范畴论的数学基础研究进路》文中指出“数学基础”是数学学科的大本大宗,数学知识建立在数学基础之上,因而数学基础的研究至关重要。集合论中悖论的出现,直接导致了数学基础危机的爆发,产生了持续已久的数学基础争论。因此,解决数学基础危机,找寻一个合适的数学基础就成为了数学哲学家迫切需要解决的问题。结构主义作为二十世纪数学哲学的研究趋势,与范畴论结合产生了范畴结构主义的研究思想,在此基础上,我们提出了基于范畴论的数学基础研究进路,为数学基础研究打开了新的思路,提供了新的可能。本论文系统地分析了基于范畴论的数学基础研究进路,论述了范畴论作为数学基础的可行性。第一章指出了包括朴素集合论、公理化集合论以及三大数学流派这些数学基础进路的困境,再通过强调数学哲学中的结构主义研究趋势,表明了数学基础研究的结构主义转向,最后指明了由范畴结构主义导出的基于范畴论的数学基础研究进路。第二章剖析了范畴论数学基础的理论内涵,沿着“数学——结构——范畴”的路线阐述了范畴论数学基础的解释路径,具体探讨了数学的本质,范畴论对数学结构的阐释以及范畴论数学基础的意义建构。第三章对数学哲学家提议的ETCS公理系统与CCAF公理系统进行了语境分析。首先明晰了范畴与语境之间的共通性,再从历史的、社会的、学术的、心理的等非语言层面与语形、语义及语用的语言层面解读如何从两个公理系统中构建数学整体。第四章辨析了范畴论数学基础面临的挑战与质疑,主要就范畴论是否预设了集合论的相关概念,范畴论的公理系统是否断言了存在,基础的必要性等问题进行了有力的辩护。第五章从整体出发对范畴论数学基础进行了综合考察,首先探讨了范畴论作为数学基础的自主性,继而论证了范畴论在什么意义上可以作为数学基础,最后聚焦于范畴论数学基础相对于集合论数学基础的研究优势。第六章从对数学哲学研究的推进,对科学研究的推动以及对语境分析方法的应用这些方面具体分析了范畴论数学基础的研究意义。结束语回顾了对基于范畴论的数学基础研究进路的整体阐述,肯定了该基础进路的研究价值,并展望了数学哲学在未来的发展。综上,本论文针对数学基础研究所面临的困境,提出了基于范畴论的数学基础进路,阐述了范畴论作为数学基础的解释路径,并结合语境分析方法对确定的范畴论公理系统进行了解析,同时指出了一些数学哲学家对范畴论数学基础的质疑甚或反对,并在对范畴论数学基础进行辩护的过程中,促使基于范畴论的数学基础进路得到了更详尽的诠释。再通过对范畴论数学基础的综合考察,又进一步丰富了基于范畴论的数学基础进路的合理性,最后在多重视角下分析了范畴论数学基础的研究意义。
李波[6]（2019）在《基于属性集拓扑基的形式概念分析方法及应用研究》文中研究表明形式概念分析是德国数学家Wille教授于1982年提出的一种对形式背景中的数据进行分析和知识获取的有力工具。如今,形式概念分析已被广泛用于信息检索、知识挖掘、知识推理等众多领域。在形式概念分析中,概念格的构造及应用始终是两个重要的研究方向。本文基于概念格构造存在的高时间复杂度的问题,以减小概念枚举空间为目标,着重研究了基于属性集拓扑基的形式概念分析方法及应用,即基于属性集拓扑基的形式概念的构造,基于属性集拓扑基的频繁闭项集挖掘和极小-极大关联规则挖掘,面向对象（属性）概念格规则提取和属性约简,以及概念格在社会网络中的k-等式概念挖掘算法。具体内容如下:（1）频繁闭项集的挖掘和极小-极大关联规则挖掘。频繁闭项集即为概念格中的概念的内涵,基于概念格的频繁闭项集和关联规则挖掘是形式概念分析的一个重要研究方向。基于频繁闭项集挖掘存在的高时间复杂度的问题,针对已有算法以项（属性）为单位枚举频繁闭项集的枚举空间大的特点,提出了基于属性集拓扑基的频繁闭项集挖掘方法。利用属性集拓扑基的性质,构造了一种TT-tree搜索空间。基于此空间可同时进行事务空间和属性空间上的搜索,且该空间相对已有算法的搜索空间更小。提出了基于属性集拓扑基的频繁闭项集挖掘算法TT-Miner,通过向已有频繁闭项集中添加属性集拓扑基中元素的方式枚举频繁闭项集,相对于传统的添加属性的方法,本文提出的算法具有更高的挖掘效率。提出一种新的基于TT-tree的极小-极大关联规则的快速挖掘方法。（2）概念格的构造。如何构建概念的搜索空间以减少重复概念的生成是构造高效的概念格生成算法的关键。讨论了概念格生成算法在概念的生成过程中,属性的顺序与概念的搜索空间大小之间的关系。基于属性集拓扑基的性质,将属性按照对应的拓扑基中元素的基数降序排列可有效缩小概念的搜索空间,减少重复概念的生成。给出了属性集拓扑基的生成算法和属性集上的序映射函数,进而提出了基于属性集拓扑基的概念格生成方法并设计了生成算法。实验结果表明,其概念生成效率高于目前已有算法。（3）面向对象（属性）概念格的决策规则提取和属性约简。基于面向对象（属性）的形式概念,提出了面向对象（属性）的决策规则的概念。构造了条件属性概念格及决策属性概念格外延集合上的等价关系,借助相应的等价关系,提出了面向对象（属性）决策规则获取方法。提出了保持面向对象（属性）决策规则的形式决策背景属性约简的概念,借助相关概念的区分属性构造区分函数,给出了约简的计算方法。（4）概念格在社会网络中发现等式概念。社会网络是一种对象集与属性集均为节点集合的具有对称结构的特殊的形式背景。基于现有社会网络中基于概念格构造方法的等式概念生成方法在效率方面不足的问题,利用等式概念的性质和基于属性集拓扑基的概念生成方法,提出了一种新的剪枝策略,进而给出了社会网络的k-等式概念快速生成算法。实验表明,其等式概念的生成速度较目前已有算法有明显提高。综上所述,本文对基于属性拓扑基的形式概念分析方法进行了深入研究,取得了一定的研究成果。这些成果在概念格的构建和形式概念分析的应用方面有着很好的前景。
田东阳[7]（2019）在《塔斯基的真理理论研究》文中指出本文中提到的“塔斯基的真理理论”是特指塔斯基在“真理”领域方面所做的一系列工作。而文中论述的塔斯基定理和塔斯基的真理定义正是这些工作的重要组成部分。塔斯基定理俗称塔斯基的真之不可定义性定理,是二十世纪关于语义悖论与逻辑语义学研究的一项重要成果。塔斯基通过在结构清晰的形式语言中重构了说谎者悖论,来证明任何算术充分的形式语言都不能在自身当中定义真谓词。而塔斯基的真理定义包括了塔斯基逻辑语义学以及塔斯基的语言层级论。塔斯基通过“满足”的方式在形式语言中定义了“真”概念,并通过对形式语言的层级划分达到了避免说谎者悖论的目的。本文试图通过对塔斯基定理和塔斯基的真理定义的分析,寻找其中的内在联系,以达到从整体上把握塔斯基真理理论的目的。本文大致可分为四部分。第一部分为第1章导论。这部分主要阐述塔斯基真理定义和塔斯基定理的研究背景和国内外研究现状,塔斯基对于问题所持有的倾向和处理问题所用到的方法,在历史上出现绝非偶然,其间有着许多学者们的贡献;第二部分为第2章、第3章和第4章。这部分主要在还原塔斯基定理的主要证明过程。证明过程包括,引入算术语言和公理系统PA,通过对哥德尔配数法的应用使形式语言具有表达足够多算术属性的能力,还有对于diag函数和编码函数的判定等诸多技术手段;第三部分为第5章。此部分完整地介绍了塔斯基的真理定义。这部分包括塔斯基对于真理定义所设想的形式正确和实质充分的分析,以及塔斯基用满足方式定义真理的方法论,还有塔斯基的语言层级论等方法;第四部分为第六章。这部分旨在从多个方面考虑塔斯基定理和塔斯基真理定义所带来的影响,结合塔斯基在各个领域的影响对塔斯基的真理理论做一个整体性的评述。最后,需要说明的是,塔斯基的真理理论是一个划时代的产物,与许多重要的成果都有着千丝万缕的联系,本文的评述仅在有限的范畴内进行。
高珂[8]（2018）在《真在非标准算术模型中的不可定义性》文中进行了进一步梳理证明全满足类、归纳部分满足类和归纳T-集合在可数非标准模型上的存在性与这个模型的递归饱和性等价。在此基础上,推广塔斯基的不可定义性结果,证明上述集合在可数的非标准算术模型上都是不可定义的。讨论这些不可定义集的相对可定义性,证明在通过科恩脱殊集得到的算术模型的扩张上不存在可定义的归纳部分满足类。
许道云[9]（2018）在《哥德尔不完全定理与数学认知的局限性——基于递归论解读哥德尔不完全定理》文中研究说明哥德尔不完全定理揭示了数学认知的局限性,任何一个含有初等数论及一阶谓词逻辑的形式证明系统中,都存在这样的命题,在此（封闭）系统中,依靠系统中的公理及一阶逻辑演算方法,既不能证明该命题为真,也不能证明它为假。哥德尔在定理的证明中开启可计算理论（递归论）之门,用现在成熟递归论的结果重新认识哥德尔不完全定理,使其变得更容易接受。近年来,机器学习取得突破性成果,由此引发有关人工智能是否可以完全代替人的思维能力等热点问题讨论。针对这一问题,如果承认"人工智能"是在一个交互计算系统中完成的,那么哥德尔不完全定理给出的是否定回答。
李春淼[10]（2018）在《向量加法系统相关模型的下界研究》文中研究指明软件的安全性问题越来越突出,当下,除了应用同行评审和软件测试等进行验证外,还可应用形式化验证在项目早期尽快发现软件缺陷。形式化验证指采取数学方式对软件系统建模并分析,目的是通过严格的数学推理来建立正确的系统。而且,对于一些要求较高安全性的系统而言,形式化方法是最佳的验证技巧。对这些系统的验证一般是通过提供基于系统的抽象数学模型上的形式化证明、数学模型和被验证的系统之间的相关性来实现的。当前,用于建模系统的一些数学模型包括:有限状态集,标记迁移系统,Petri网,向量加法系统,时间自动机,进程代数等。并发理论是理论计算机科学中众多一直比较活跃的研究领域之一。一些用于建模和验证并发系统的形式化模型被相继提出,比如Petri网和向量加法系统、进程演算等。尽管Petri网主要是提供在物理世界上的计算方法,而向量加法系统主要用于并发编程的形式化模型,但之后他们被证明是数学上等价的。向量加法系统由有限个整数向量组成,系统的格局是自然数向量的集合,每一步的迁移是对当前的格局应用一个整数向量而到达另一个格局。向量加法系统上的一些研究主要围绕的问题包括可达性问题、可覆盖性问题等。为了增加向量加法系统的表达能力,在其基础上进行扩增又衍生出了一些其他模型,如带状态的向量加法系统、递归向量加法系统、交替向量加法系统等。Cai和Ogawa将下推系统和向量加法系统相结合,提出良结构下推系统,可用于建模递归多线程程序。良结构下推系统具有强大的表达能力,向量加法系统及一些对其扩展的模型可被规约到良结构下推系统上,例如分支向量加法系统、递归向量加法系统等。因此,良结构下推系统的研究结论可直接被用于这些模型上。尽管向量加法系统的扩展模型的一些可覆盖性问题还未被解决,但可以对该问题的难度进行一定的衡量,即可以通过寻找该问题难度的上界和下界,通过二者之间差距的不断缩小而确定。本文提出一个用于证明模型可覆盖性问题下界的一般性框架,并基于重置0（即不测试一个变量值的情况下直接对其赋值为0）,利用规约的方式得到下界。基于本文提出的框架,验证了下推向量加法系统的可覆盖性问题的难度下界为TOWER难的,与已知的Lazic提出的下界难度相一致。并证明了对以3维自然数向量为状态的且栈字符集有限的良结构下推系统和状态集有限且以3维自然数向量为栈字符集的良结构下推系统,其可覆盖性问题的难度下界是Ackermann难的;状态集有限且栈字符集为n+3维良拟序集的良结构下推系统,其可覆盖性问题的下界是Hyper-Ackermann难的。本文还提出良结构的带有范围限制匹配关系的多栈下推系统（简记为WSMPDS）,对多栈下推系统中的弹栈操作进行限制,即仅当一个栈顶符号是上k个轮回里被压入栈中的才可被执行弹栈操作（其中k为某个固定的常量）,而且栈字符集为良拟序集,然后介绍其可覆盖性问题的定义。并通过向量加法系统的可覆盖性问题到此模型的可覆盖性问题的规约,得出了其可覆盖性问题的下界是EXPSPACE难的。
二、关于自然数集合上的递归定理（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、关于自然数集合上的递归定理（论文提纲范文）
（1）基于Coq的Paxos的形式化建模与验证（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第一章 绪论 |
| 1.1 研究背景与意义 |
| 1.2 分布式一致性及其形式化验证的研究现状概述 |
| 1.3 研究内容和目标 |
| 1.4 相关工作 |
| 1.5 论文结构 |
| 第二章 分布式共识与Paxos |
| 2.1 副本复制技术 |
| 2.2 Basic Paxos |
| 2.2.1 CAP理论 |
| 2.2.2 Quorum系统 |
| 2.2.3 分布式共识 |
| 2.2.4 Basic Paxos |
| 2.2.5 Basic Paxos总结 |
| 2.3 本章小结 |
| 第三章 交互式定理证明系统Coq |
| 3.1 Coq系统组成 |
| 3.1.1 证明开发系统 |
| 3.1.2 证明检查器 |
| 3.2 Coq交互式开发环境 |
| 3.3 Coq语法简介 |
| 3.3.1 基本概念 |
| 3.3.2 模式匹配结构 |
| 3.3.3 归纳数据类型 |
| 3.3.4 Record类型 |
| 3.3.5 证明策略 |
| 3.3.6 证明方法和思路 |
| 3.4 本章小结 |
| 第四章 Basic Paxos的形式化建模 |
| 4.1 准备工作 |
| 4.2 Basic Paxos基本数据结构的形式化定义 |
| 4.2.1 Basic Paxos主要角色的形式化定义 |
| 4.2.2 Coq集合标准库引理的扩充及证明 |
| 4.2.3 Basic Paxos的投票行为 |
| 4.2.4 Basic Paxos的消息抽象 |
| 4.3 Basic Paxos的系统状态 |
| 4.3.1 Basic Paxos三大前提条件抽象 |
| 4.4 Basic Paxos实例 |
| 4.5 本章小结 |
| 第五章 Basic Paxos的形式化验证 |
| 5.1 Basic Paxos重要性质的归纳定义 |
| 5.1.1 Basic Paxos共识语义的归纳定义 |
| 5.1.2 Basic Paxos消息流程的归纳定义 |
| 5.2 Basic Paxos的形式化验证 |
| 5.3 本章小结 |
| 第六章 结束语 |
| 6.1 论文总结 |
| 6.2 工作展望 |
| 附录A Coq代码 |
| 参考文献 |
| 致谢 |
| 攻读硕士学位期间发表论文和科研情况 |
（2）基于Coq的“模”观点下线性代数机器证明系统 ——特例：模分解定理的机器证明（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.1.1 研究背景 |
| 1.1.2 研究意义 |
| 1.2 国内外发展现状 |
| 1.3 模观点下的线性代数简介 |
| 1.4 交互式定理证明工具Coq简介 |
| 1.5 本文研究内容及结构安排 |
| 第二章 Coq的基础内容 |
| 2.1 Coq的基本语法 |
| 2.1.1 构造演算 |
| 2.1.2 归纳构造 |
| 2.2 公理化集合论形式化系统 |
| 第三章 基本代数结构的Coq形式化 |
| 3.1 群、环、域等代数结构的形式化 |
| 3.2 素元因子分解定理的机器证明 |
| 第四章 模及其分解定理的形式化 |
| 4.1 线性代数与其上模的形式化 |
| 4.1.1 向量空间与线性变换 |
| 4.1.2 模的基本概念与性质 |
| 4.1.3 向量空间与模的差异 |
| 4.2 主理想整环上有限生成模分解定理的机器证明 |
| 4.2.1 有限生成模分解定理的机器证明 |
| 4.2.2 准素唯一分解定理的机器证明 |
| 4.2.3 循环分解唯一性定理的机器证明 |
| 第五章 总结与展望 |
| 5.1 研究总结 |
| 5.2 研究展望 |
| 参考文献 |
| 致谢 |
（3）基于定理证明器Coq的形式语义验证研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 研究背景与动机 |
| 1.2 研究现状与相关工作 |
| 1.3 本文的主要工作 |
| 1.4 本文组织结构 |
| 第二章 基础理论与指导方法 |
| 2.1 多线程离散事件仿真语言 |
| 2.2 统一建模语言 |
| 2.3 形式语义学 |
| 2.4 程序统一理论 |
| 2.5 定理证明器Coq |
| 2.6 本章小结 |
| 第三章 MDESL代数语义与操作语义连接的机械验证 |
| 3.1 MDESL代数语义介绍及其机械定义 |
| 3.2 从代数语义生成的操作语义介绍及其机械验证 |
| 3.3 生成策略与派生操作语义等价性的机械验证 |
| 3.4 本章小结 |
| 第四章 MDESL指称语义与代数定律正确性的机械验证 |
| 4.1 离散时间语义模型介绍及其机械验证 |
| 4.2 基于离散时间语义模型的指称语义介绍及其机械定义 |
| 4.3 代数定律的机械验证 |
| 4.4 本章小结 |
| 第五章 UML类图形式语义与精化关系的机械验证 |
| 5.1 类图抽象语法介绍及其机械定义 |
| 5.2 类图良构规则机械定义 |
| 5.3 类图精化关系介绍及其机械验证 |
| 5.4 本章小结 |
| 第六章 UML静态模型一致性的机械定义与验证 |
| 6.1 对象图介绍及其机械定义 |
| 6.2 UML静态模型一致性的机械定义与验证 |
| 6.3 UML模型到Coq代码的自动转换工具 |
| 6.4 基于定理证明器Coq的可机械验证UML框架 |
| 6.5 本章小结 |
| 第七章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 后续工作展望 |
| 参考文献 |
| 附录 |
| A 并行展开定律 |
| B 顺序组合的机械验证 |
| C 并行进程的操作语义的机械定义 |
| D 健康公式hold相关属性的机械验证 |
| E MDESL的指称语义介绍 |
| F 连续Skip代数定律的机械证明 |
| 致谢 |
| 攻读博士学位期间发表论文和科研情况 |
（4）限制分拆的算术性质和Catalan数的研究（论文提纲范文）
| 中文摘要 |
| 英文摘要 |
| 1 绪论 |
| 1.1 问题的研究背景和发展现状 |
| 1.2 本文内容介绍 |
| 2 2-着色分拆三元组数模3和5高次幂的同余性质 |
| 2.1 问题的提出和主要结果 |
| 2.2 预备知识和引理 |
| 2.3 模3高次幂的同余式的证明 |
| 2.4 模5和5 的高次幂同余式的证明 |
| 2.5 本章注记 |
| 3 k-着色分拆数模5幂次的同余性质 |
| 3.1 问题的提出和主要结果 |
| 3.2 模25 的同余式的证明 |
| 3.3 模5高次幂的同余式的证明 |
| 3.4 本章注记 |
| 4 k-着色分拆数的一些不等式 |
| 4.1 问题的提出主要结果 |
| 4.2 第一个证明-代数证明 |
| 4.3 第二个证明-组合证明 |
| 4.4 本章注记 |
| 5 关于k-着色分拆的广义奇异秩 |
| 5.1 问题的提出和主要结果 |
| 5.2 k-曲秩模2,3,和4 的不等式的证明 |
| 5.3 加权对称化的2-奇异秩和3-奇异秩的矩 |
| 5.4 本章注记 |
| 6 (q,t)-Catalan数：gamma分解,禁模式,和(-1)-现象 |
| 6.1 问题的提出和主要结果 |
| 6.2 定义和引理 |
| 6.3 定理的证明以及q-Narayana多项式的一个变形 |
| 6.4 禁模式集合上(-1)-现象的一个完全刻画 |
| 6.5 本章注记 |
| 7 结论与展望 |
| 参考文献 |
| 附录 |
| A 作者在攻读博士学位期间的工作 |
| B 作者在攻读博士学位期间参加科研项目 |
| C 学术兼职 |
| D 学位论文数据集 |
| 致谢 |
（5）基于范畴论的数学基础研究进路（论文提纲范文）
| 中文摘要 |
| ABSTRACT |
| 绪论 |
| 第一章 数学基础研究的结构主义转向 |
| 1.1 传统数学基础进路的困境 |
| 1.1.1 朴素集合论及其困境 |
| 1.1.2 公理化集合论的发展及难题 |
| 1.2 三大数学流派的挫败 |
| 1.2.1 逻辑主义 |
| 1.2.2 形式主义 |
| 1.2.3 直觉主义 |
| 1.3 数学哲学中的结构主义研究趋势 |
| 1.3.1 数学结构主义的兴起与发展 |
| 1.3.2 先物结构主义及模态结构主义难题 |
| 1.3.3 范畴结构主义 |
| 1.4 小结 |
| 第二章 范畴论数学基础的基本涵义 |
| 2.1 数学的本质——结构 |
| 2.1.1 数学本质的多元分析 |
| 2.1.2 数学结构的解释说明 |
| 2.1.3 数学本质的结构解析 |
| 2.2 范畴论对数学结构的阐释 |
| 2.2.1 范畴的概念表征 |
| 2.2.2 范畴的结构特性 |
| 2.2.3 数学结构的理论 |
| 2.3 范畴论数学基础的意义建构 |
| 2.3.1 诠释数学内核 |
| 2.3.2 构建数学框架 |
| 2.4 小结 |
| 第三章 范畴论数学基础的语境分析 |
| 3.1 范畴论数学基础的语境基底 |
| 3.1.1 表述特征:整体性与动态性 |
| 3.1.2 发展源由:内在成因及外在动因 |
| 3.2 ETCS公理系统的语境分析 |
| 3.2.1 ETCS公理系统的非语言分析 |
| 3.2.2 ETCS公理系统的语言分析 |
| 3.3 CCAF公理系统的语境分析 |
| 3.3.1 CCAF公理系统的非语言分析 |
| 3.3.2 CCAF公理系统的语言分析 |
| 3.4 范畴论数学基础的语境分析意义 |
| 3.5 小结 |
| 第四章 范畴论数学基础的理性辩护 |
| 4.1 对范畴论的认识 |
| 4.1.1 概念分析 |
| 4.1.2 全域说明 |
| 4.1.3 内容阐述 |
| 4.2 对公理的辨析 |
| 4.2.1 断言 |
| 4.2.2 公理化方法 |
| 4.2.3 公理系统 |
| 4.3 对数学基础的理解 |
| 4.3.1 基础的必要性 |
| 4.3.2 语言与基础 |
| 4.3.3 框架与基础 |
| 4.4 小结 |
| 第五章 范畴论数学基础的综合考察 |
| 5.1 自主性论证 |
| 5.1.1 逻辑的自主性 |
| 5.1.2 概念的自主性 |
| 5.1.3 辩护的自主性 |
| 5.2 意义分析 |
| 5.2.1 本体论的数学基础探究 |
| 5.2.2 认识论的数学基础探究 |
| 5.2.3 方法论的数学基础探究 |
| 5.3 研究优势 |
| 5.3.1 研究特点 |
| 5.3.2 阐释的充分性 |
| 5.4 小结 |
| 第六章 范畴论数学基础的研究意义 |
| 6.1 对数学哲学研究的推进 |
| 6.1.1 数学基础 |
| 6.1.2 数学结构主义 |
| 6.2 对科学研究的推动 |
| 6.2.1 数学学科 |
| 6.2.2 其他学科 |
| 6.3 对语境分析方法的推广 |
| 6.4 小结 |
| 结束语 |
| 参考文献 |
| 攻读学位期间取得的研究成果 |
| 致谢 |
| 个人简况及联系方式 |
（6）基于属性集拓扑基的形式概念分析方法及应用研究（论文提纲范文）
| 摘要 |
| abstract |
| 第1章 绪论 |
| 1.1 课题研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 形式概念分析理论的研究现状 |
| 1.2.2 形式概念分析应用的研究现状 |
| 1.3 本文的研究内容 |
| 1.4 论文结构 |
| 第2章 预备知识 |
| 2.1 形式概念分析基础 |
| 2.2 概念格的扩展模型 |
| 2.2.1 面向属性的概念格 |
| 2.2.2 面向对象的概念格 |
| 2.3 频繁项集 |
| 2.4 概念格生成算法概述 |
| 2.5 本章小结 |
| 第3章 形式背景的拓扑事务树及其算法 |
| 3.1 属性之间的相似关系及其拓扑空间 |
| 3.2 经典的频繁闭项集挖掘算法 |
| 3.3 事务数据库的拓扑事务树生成算法 |
| 3.3.1 事务数据库的拓扑基生成算法 |
| 3.3.2 拓扑事务树生成算法 |
| 3.4 TT-tree中的频繁闭项集生成算法 |
| 3.5 TT-tree中挖掘极小-极大关联规则 |
| 3.5.1 挖掘可信度为1的极小-极大关联规则 |
| 3.5.2 挖掘可信度小于1的极小-极大关联规则 |
| 3.6 实验分析 |
| 3.6.1 挖掘频繁闭项集 |
| 3.6.2 按比例扩大实验 |
| 3.6.3 项的空间和拓扑基空间的比较 |
| 3.7 本章小结 |
| 第4章 基于属性拓扑基的形式概念快速生成算法 |
| 4.1 形式概念生成算法 |
| 4.1.1 CbO形式概念生成算法 |
| 4.1.2 FCbO形式概念生成算法 |
| 4.2 基于属性集拓扑基的FCbO算法 |
| 4.2.1 属性的拓扑基生成算法 |
| 4.2.2 形式概念的枚举空间 |
| 4.2.3 TFCbO算法 |
| 4.2.4 时间复杂度分析 |
| 4.3 实验分析 |
| 4.4 本章小结 |
| 第5章 基于概念格的属性约简和决策规则提取 |
| 5.1 基于面向对象概念格的规则获取和属性约简 |
| 5.1.1 形式决策背景的决策规则 |
| 5.1.2 基于面向对象概念格的决策规则 |
| 5.1.3 面向对象概念格的属性约简 |
| 5.2 基于面向属性概念格的规则提取和属性约简 |
| 5.2.1 基于面向属性概念格的决策规则 |
| 5.2.2 基于面向属性概念格的属性约简 |
| 5.3 本章小结 |
| 第6章 基于形式概念分析的社会网络挖掘算法 |
| 6.1 社会网络基础知识 |
| 6.2 k-等式概念快速生成算法EC-TFCb O |
| 6.3 实验分析 |
| 6.4 本章小结 |
| 结论与展望 |
| 致谢 |
| 参考文献 |
| 攻读博士学位期间发表的论文及科研成果 |
（7）塔斯基的真理理论研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 选题意义 |
| 1.2 时代背景 |
| 1.3 国内外研究现状 |
| 第2章 罗素悖论 |
| 2.1 直观上的对角线思想 |
| 2.2 对角线版本的罗素悖论 |
| 第3章 塔斯基定理 |
| 3.1 形式化 |
| 3.1.1 形式化语言 |
| 3.1.2 哥德尔编码 |
| 3.2 塔斯基定理的证明 |
| 3.2.1 对角化引理 |
| 3.2.2 真的不可定义性 |
| 第4章 L_A中的判定问题 |
| 4.1 能行可判定与能行可计算 |
| 4.2 原始递归函数 |
| 4.2.1 更多的原始递归函数 |
| 4.2.2 diag函数的构造 |
| 4.2.3 编码函数的构造 |
| 4.3 L_A可表达所有的原始递归函数 |
| 第5章 满足的定义与语言分层 |
| 5.1 实质充分与形式正确 |
| 5.2 满足的定义 |
| 5.2.1 满足的直观上说明 |
| 5.2.2 严格的满足定义 |
| 5.3 对象语言与元语言 |
| 5.3.1 语言层次论 |
| 5.3.2 无穷阶语言 |
| 第6章 塔斯基真理理论的方法论意义 |
| 6.1 对悖论研究的影响 |
| 6.2 对逻辑语义学的贡献 |
| 6.3 真与可证的区分 |
| 6.4 对演绎科学的影响 |
| 6.5 真值条件理论 |
| 结语 |
| 致谢 |
| 参考文献 |
| 攻读硕士期间发表的论文及参加的学术科研活动 |
（10）向量加法系统相关模型的下界研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 主要符号对照表 |
| 第一章 绪论 |
| 1.1 研究背景 |
| 1.2 研究内容 |
| 1.3 章节安排 |
| 第二章 背景知识 |
| 2.1 向量加法系统 |
| 2.2 下推系统 |
| 2.3 良结构下推系统 |
| 2.4 时间/空间复杂性 |
| 2.5 规约 |
| 2.6 2-计数机器 |
| 2.6.1 Hyper-Ackermann函数 |
| 2.6.2 Ackermann函数 |
| 2.7 本章小结 |
| 第三章 证明模型可覆盖性问题下界的一般性框架 |
| 3.1 主要规约思路 |
| 3.2 有界的 2-计数机器的模拟 |
| 3.3 函数f(?) 的正向计算和逆向计算 |
| 3.4 本章小结 |
| 第四章 验证下推向量加法系统的可覆盖性问题下界 |
| 4.1 (正向)弱计算TOWER函数 |
| 4.2 (逆向)弱计算TOWER函数 |
| 4.3 本章小结 |
| 第五章 良结构下推系统的可覆盖性问题下界 |
| 5.1 状态为向量 |
| 5.1.1 (正向) 弱计算Ackermann函数 |
| 5.1.2 (逆向) 弱计算Ackermann函数 |
| 5.2 栈字符为向量 |
| 5.2.1 Ackermann难的下界结果 |
| 5.2.2 Hyper - Ackermann难的下界结果 |
| 5.3 本章小结 |
| 第六章 良结构的带有范围限制匹配关系的多栈下推系统的可覆盖性问题的下界 |
| 6.1 良结构的带有范围限制匹配关系的多栈下推系统 (WSMPDS) |
| 6.2 WSMPDS的可覆盖性问题的下界 |
| 6.3 本章小结 |
| 第七章 相关工作 |
| 7.1 可覆盖性和可达性结果 |
| 7.2 向量加法系统的下界 |
| 7.3 良结构下推系统表达能力 |
| 7.3.1 分支向量加法系统 |
| 7.3.2 带状态的下推向量加法系统 |
| 7.3.3 递归向量加法系统 |
| 7.3.4 交替向量加法系统 |
| 7.4 本章小结 |
| 第八章 总结与未来展望 |
| 参考文献 |
| 致谢 |
| 攻读学位期间发表的学术论文 |
| 攻读学位期间参与的项目 |
四、关于自然数集合上的递归定理（论文参考文献）
- [1]基于Coq的Paxos的形式化建模与验证[D]. 李亚男. 华东师范大学, 2020(10)
- [2]基于Coq的“模”观点下线性代数机器证明系统 ——特例：模分解定理的机器证明[D]. 范一凡. 北京邮电大学, 2020(05)
- [3]基于定理证明器Coq的形式语义验证研究[D]. 盛枫. 华东师范大学, 2019(06)
- [4]限制分拆的算术性质和Catalan数的研究[D]. 唐大钊. 重庆大学, 2019(09)
- [5]基于范畴论的数学基础研究进路[D]. 孔祥雯. 山西大学, 2019(01)
- [6]基于属性集拓扑基的形式概念分析方法及应用研究[D]. 李波. 西南交通大学, 2019(06)
- [7]塔斯基的真理理论研究[D]. 田东阳. 武汉理工大学, 2019(07)
- [8]真在非标准算术模型中的不可定义性[J]. 高珂. 重庆理工大学学报(社会科学), 2018(11)
- [9]哥德尔不完全定理与数学认知的局限性——基于递归论解读哥德尔不完全定理[J]. 许道云. 贵州大学学报(自然科学版), 2018(03)
- [10]向量加法系统相关模型的下界研究[D]. 李春淼. 上海交通大学, 2018(01)