导读:本文包含了形式化数学论文开题报告文献综述及选题提纲参考文献，主要关键词:形式化方法,程序规约,组合数学,递推技术
形式化数学论文文献综述
熊小超,杨庆红[1]（2019）在《2类组合数学问题的算法形式化推导》一文中研究指出组合数学问题算法的研究是计算机科学的重要研究内容,但在许多相关文献中,许多组合数学问题的算法只是经过简单分析得到,并未给出算法程序的详细设计过程,导致读者无法理解算法本质,更无法保证算法程序的正确性.该文在以组合数学中连续子序列最大乘积和第2类斯特林数变形问题为例的基础上,通过形式化描述问题的程序规约,使用规约变换规则,对程序规约进行一系列等价变换,获得问题求解序列的递推式,并以此为基础得到问题求解的算法程序,清晰地展示了从问题的需求到算法程序的详细推导过程.通过对相关组合数学问题的进一步深入研究,提炼了2类组合数学问题的求解策略,为提高组合数学问题算法程序的正确性提供了有效途径.(本文来源于《江西师范大学学报(自然科学版)》期刊2019年04期）
陈曦[2]（2019）在《基于Coq的直升机形式化飞行控制数学初步探索》一文中研究指出定理证明是人工智能的一个分支,它的研究目标是在计算机辅助下进行数学定理的证明。基于定理证明的形式化验证技术已经被广泛应用于数学定理的证明验证以及软件正确性验证。然而定理证明技术在工程数学中的应用还十分罕见。安全飞行控制系统在飞行控制中扮演了一个重要的角色并且被认为是飞机的“大脑”。只有该系统被验证为正确的飞机才能安全稳定的飞行。飞行控制算法是飞行控制系统的核心,它的基础是大量繁复的微积分数学推导,这些数学推导的正确性对飞行控制系统的安全性有关键性作用。欧洲曾经发生由于下降过程控制的失误导致火星着陆的失败。在直升机飞行控制数学的形式化验证方面,目前国际上是空白。本文是基于定理证明器Coq对直升机飞行控制系统中的部分数学公式的推导进行的形式化验证初步探索,主要研究内容如下:第一,对以显模型跟踪控制系统为基础的直升机自动过渡飞行控制过程进行验证。这一过程分为高度过渡和速度过渡两个方面,其中高度又分抛物线下降和指数拉平两个阶段。这两个阶段本身受相应的物理定律和控制目标约束,两者之间需要平滑的连接。下降曲线所满足的数学公式来源于在这些约束条件下的推导。我们对这一推导过程进行了形式化描述和验证。第二,对直升机舰上起飞过程及轨迹生成进行验证。该过程在时间上分为叁个时间段即开始阶段,稳定上升阶段和终段,在空间上简化为忽略Y轴只考虑XOZ平面,在平面内通过初始状态和任务要求在保证轨迹平滑的情况下设定运动方程。验证过程中我们证明了几个自定义小引理。第叁,对直升机着舰过程及轨迹生成进行验证。着舰比舰上起飞要困难,因为要考虑叁个方面的因素即甲板尺寸有限、舰船晃动、直升机自身控制减弱。第四,Z变换形式化验证。Z变换能够把一系列实数或复数离散信号从时域转换成复频域,是控制系统中的重要分析手段。由于Coq标准库及第叁方库中有关复数的定理相对缺乏,所以我们从复数形式化开始,通过欧拉公式等手段对复数进行转换和简化,然后在此基础上验证了Z变换的齐次,均匀,线性,以及复数位移性质,由此来扩展定理证明工具在系统分析方面的能力,同时为进一步形式化直升机飞控系统奠定了基础。(本文来源于《南京航空航天大学》期刊2019-03-01）
陈平[3]（2019）在《数学形式化的境域性教学》一文中研究指出数学形式化教学是数学抽象核心素养培养的重要途径,形式化的适度性是教学的一个难题。把形式化置于境域性知识的观点之下进行教学,从知识产生、主观建构、数学本质叁个维度,整合了过程认同、动态创生、数学辩护的境域性教学策略,以此把握形式化程度,促进学生形式化知识的建构和数学抽象素养的形成。(本文来源于《学园》期刊2019年01期）
邓平升[4]（2018）在《用形式化原则指导数学解题教学——以求直线方程的教学为例》一文中研究指出在高中数学解题中,形式化原则有着极为重要的地位,对于培养学生的发散思维和分析解答问题的能力有着不可替代的作用.形式化原则指的是同一个数学问题可以用不同的形式表述出来,同一个形式又可以反应出不同的数学模型、数学内容.在教学中,教师通过形式化原则指导学生解题,可以培养学生从多角度去分析问题,运用化归思想进行解题的能力.下面本文以求直线方程的教学为例来探讨如何运用形式化原则指导解题教学.(本文来源于《语数外学习(高中版中旬)》期刊2018年09期）
林辉庆[5]（2018）在《数学的形式化特征及其在物理中的应用》一文中研究指出数学是研究现实世界的数量关系和空间形式的科学,是学习和研究其他定量学科的基础和工具,形式化是它的本质特征之一。由于数学的形式化特征,两个物理现象如果有相同的数学结构,则必定有相同的数学结果;如果有相同的数学结果,则可能有相同的数学结构。这在物理研究和物理学习中有重要的应用。(本文来源于《物理教学》期刊2018年08期）
黄忠环[6]（2018）在《小学数学合作学习形式化现象剖析及对策》一文中研究指出新课程改革以来,合作学习被作为有效的学习方式充分地应用于小学数学课中,在课堂教学实践中,很多一线教师在开展合作学习时,由于在认识上存在不足,导致在操作层面出现了多种的问题,这需要教师进行有效的反思并克服。本文结合教学案例深入剖析了小学数学合作学习存在的问题,并在此基础上提出了相应的对策。(本文来源于《数学教学通讯》期刊2018年07期）
曹志栋[7]（2017）在《谈数学形式化与非形式化的转化》一文中研究指出《普通高中数学课程标准》把"强调本质,注意适度形式化"作为课程的基本理念之一,形式化是数学的本质特征之一,但过度的形式化又会让学生感觉到数学只是堆积起来的一堆符号,失去了数学应有的应用性质,会导致学生的数学应用意识薄弱,不能抓住数学知识的本质,因此,在数学教学中实现数学形式化与非形式化的转化是一项颇具难度的工作.本文将结合笔者在教学工作中的体会,提出一些建议.(本文来源于《数学学习与研究》期刊2017年18期）
游颖[8]（2017）在《算法形式化方法在叁类组合数学问题求解中的应用研究》一文中研究指出算法设计是计算机科学研究的重要领域之一。目前计算机科学处理的大部分数据都是离散的数据,而组合数学是研究离散数据的科学,因此研究以组合数学为基础的算法的可靠性、正确性和生产效率就成为算法设计领域中的关键问题。对于求解组合数学相关的问题,目前存在多种算法设计方法,形式化开发方法是其中之一。形式化方法的本质是基于数学的方法来描述、开发和验证目标软件系统的一种技术,使用形式化方法开发算法程序能有效提高算法程序设计的规范化、自动化程度以及算法的可靠性和正确性。基于递推技术的算法形式化方法在部分形式化或者是完全形式化描述问题程序规约的基础上,通过对问题的程序规约进行数学变换,得到问题求解的递推关系,在此基础上得到最终的算法程序。由于求解问题的递推关系建立在严格数学变换的基础上,因而递推关系的正确性得到了保证,从而也有效确保最终的算法程序的正确性;另外,使用该方法开发算法程序,均是以寻找问题求解序列的递推关系为出发点,先得到较小的子问题的解,再在之前已获得的较小子问题解的基础上直接或间接得到较大问题的解,这样可以避免很多不必要的重复计算,从而有效提高算法程序的效率,并为算法程序的开发提供一条较为统一的途径。本文重点研究了基于递推关系的算法形式化方法在叁类典型组合数学问题求解中的应用。本文分析了当前形式化开发方法的需求以及发展状况;介绍了基于递推技术的形式化开发方法的开发语言、开发步骤以及关键技术等,同时研究了它在组合数学问题开发上的有效性;接着,本文针对组合数学问题进行分类研究,使用基于递推技术的形式化方法开发了叁类有代表性的组合数学问题:整除问题、排列组合问题以及NP完全问题中的0-1背包变形问题,同时在分析每一类问题形式化开发过程共性的基础上提炼得到了求解该类问题的统一策略,并将其推广到相似问题的求解;最后对基于递推关系的形式化开发方法在组合数学上的应用进行了总结。研究表明,基于递推技术的算法形式化开发方法有效保证了算法程序的正确性,提高了算法程序的执行效率。(本文来源于《江西师范大学》期刊2017-05-01）
周余峰[9]（2017）在《小议数学教学中核心素养之数学抽象的非形式化演绎》一文中研究指出新一轮数学课程标准已经制定完毕,核心素养作为本轮课标的关键被多次提及。数学知识的形式化是数学特有的特征之一,如何从非形式化的角度较好地演绎,成为教学关键。(本文来源于《数学大世界(中旬)》期刊2017年04期）
李娟[10]（2016）在《从“形式化定义”走向“数学内涵”——以小学数学概念教学中“推理能力”的培养为例》一文中研究指出"推理能力"是"课标2011年版"中数学学习的十个核心概念之一,推理的理性精神价值和实际应用价值,决定了其在数学教学中的特殊地位。小学数学概念教学是小学阶段数学教学的基础内容,实际教学中,以定义代概念的"形式化"的教学方式依然存在。本文根据小学数学概念的特点、学生的认知规律和心理特征,通过引导学生经历概念学习过程,努力构建具有"数学内涵"的概念认识课堂,从而有效促进学生推理能力的发展。(本文来源于《小学数学教师》期刊2016年09期）
形式化数学论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
定理证明是人工智能的一个分支,它的研究目标是在计算机辅助下进行数学定理的证明。基于定理证明的形式化验证技术已经被广泛应用于数学定理的证明验证以及软件正确性验证。然而定理证明技术在工程数学中的应用还十分罕见。安全飞行控制系统在飞行控制中扮演了一个重要的角色并且被认为是飞机的“大脑”。只有该系统被验证为正确的飞机才能安全稳定的飞行。飞行控制算法是飞行控制系统的核心,它的基础是大量繁复的微积分数学推导,这些数学推导的正确性对飞行控制系统的安全性有关键性作用。欧洲曾经发生由于下降过程控制的失误导致火星着陆的失败。在直升机飞行控制数学的形式化验证方面,目前国际上是空白。本文是基于定理证明器Coq对直升机飞行控制系统中的部分数学公式的推导进行的形式化验证初步探索,主要研究内容如下:第一,对以显模型跟踪控制系统为基础的直升机自动过渡飞行控制过程进行验证。这一过程分为高度过渡和速度过渡两个方面,其中高度又分抛物线下降和指数拉平两个阶段。这两个阶段本身受相应的物理定律和控制目标约束,两者之间需要平滑的连接。下降曲线所满足的数学公式来源于在这些约束条件下的推导。我们对这一推导过程进行了形式化描述和验证。第二,对直升机舰上起飞过程及轨迹生成进行验证。该过程在时间上分为叁个时间段即开始阶段,稳定上升阶段和终段,在空间上简化为忽略Y轴只考虑XOZ平面,在平面内通过初始状态和任务要求在保证轨迹平滑的情况下设定运动方程。验证过程中我们证明了几个自定义小引理。第叁,对直升机着舰过程及轨迹生成进行验证。着舰比舰上起飞要困难,因为要考虑叁个方面的因素即甲板尺寸有限、舰船晃动、直升机自身控制减弱。第四,Z变换形式化验证。Z变换能够把一系列实数或复数离散信号从时域转换成复频域,是控制系统中的重要分析手段。由于Coq标准库及第叁方库中有关复数的定理相对缺乏,所以我们从复数形式化开始,通过欧拉公式等手段对复数进行转换和简化,然后在此基础上验证了Z变换的齐次,均匀,线性,以及复数位移性质,由此来扩展定理证明工具在系统分析方面的能力,同时为进一步形式化直升机飞控系统奠定了基础。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
形式化数学论文参考文献
[1].熊小超,杨庆红.2类组合数学问题的算法形式化推导[J].江西师范大学学报(自然科学版).2019
[2].陈曦.基于Coq的直升机形式化飞行控制数学初步探索[D].南京航空航天大学.2019
[3].陈平.数学形式化的境域性教学[J].学园.2019
[4].邓平升.用形式化原则指导数学解题教学——以求直线方程的教学为例[J].语数外学习(高中版中旬).2018
[5].林辉庆.数学的形式化特征及其在物理中的应用[J].物理教学.2018
[6].黄忠环.小学数学合作学习形式化现象剖析及对策[J].数学教学通讯.2018
[7].曹志栋.谈数学形式化与非形式化的转化[J].数学学习与研究.2017
[8].游颖.算法形式化方法在叁类组合数学问题求解中的应用研究[D].江西师范大学.2017
[9].周余峰.小议数学教学中核心素养之数学抽象的非形式化演绎[J].数学大世界(中旬).2017
[10].李娟.从“形式化定义”走向“数学内涵”——以小学数学概念教学中“推理能力”的培养为例[J].小学数学教师.2016