函数的微分、偏微分及梯度、散度、旋度在Mizar语言下的实现

1、函数的微分、偏微分及梯度、散度、旋度在Mizar语言下的实现 青岛科技大学硕士学位论文函数的微分、偏微分及梯度、散度、旋度在Mizar语言下的实现姓名:谢冰申请学位级别:硕士专业:应用数学指导教师:梁希泉20090610青岛科技人学研究生学位论文函数的微分、偏微分及梯度、散度、旋度在语言下的实现摘要系统是一种计算机语言系统,是集逻辑证明、推理演绎、复杂计算、校验排版、科研教学于一体的处理数学信息的形式化系统,并拥有自己的数学知识数据库。本文首先介绍数学机械化及系统的发展历史,其次对如何利用语言完成数学论文的撰写和进行自动推理校验给出了简要的说明。本文在系统下讨论了函数偏微分、高阶偏微分理论及相

2、关性质,实现了矢量场、梯度、散度、旋度的形式,针对不同的数学问题给出了相应的算法和严格的证明,且通过了系统验证。所获结果被收录在数据库中,并以论文的形式发表在波兰 杂志上。主要工作如下:.在语言下实现了多元函数的微分,借助其微分建立起欧氏空间中二元函数偏微分定义的新形式,讨论了二元函数偏微分的运算性质及可微与连续的关系。.在系统下,首次实现了二阶偏微分的表述,定义的形式简洁明了,并完成了相应的运算公式和定理的证明与验证。.将二元函数偏微分的理论推广到三维欧氏空间中,定义了矢量场,由此在系统下第一次实现了梯度、散度、旋度的定义并将其相关的定理与运算实现了机械化。关键词:数学机械化语言系统形式化数

3、学计算机证明青岛科技大学研究生学位论文佃,.,., , .,. ,:. , ,.,., , .函数的微分、偏微分及梯度、散度、旋度在语言下的实现:, 青岛科技人学研究生学位论文声 明独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢中所罗列的内容以外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含本人已用于其他学位申请的论文或成果。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处,本人承担一切相关责任。本人签名: 日期:立年月侈日毒舸水关于论文使用授权的说明

4、本学位论文作者完全了解青岛科技大学有关保留、使用学位论文的规定,有权保留并向国家有关部门或机构送交论文的复印件和磁盘,允许论文被查阅和借阅。本人授权学校可以将学位论文的全部或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人离校后发表或使用学位论文或与该论文直接相关的学术论文或成果时,署名单位仍然为青岛科技大学。保密的学位论文在解密后适用本授权书本学位论文属于:保密口,在 年解密后适用于本声明。不保密口。请在以上方框内打“;雨冰本人签名:日期:潲年月;日日期:导师签名:。听年月,易日琴布永青岛科技人学研究生学位论文绪论.数学机械化的历史及发展现状以蒸汽机

5、为标志的工业革命开创了体力劳动机械化的时代,而以电子计算机为标志的科技革命使人类社会由工业时代进入信息时代,为实现脑力劳动的机械化提供了物质基础。数学是整个科学的基础,是联络自然科学和高科技的纽带。今天,数学已经发展成为研究一切可能的数量关系与空间形式的科学,从研究的内容、范围、意义到方法都发生了深刻的变革,数学机械化便是适应信息时代而产生的新兴研究领域。数学机械化又称为机械化方法或机器证明,其思想实质是以构造性与算法化的方式从事数学研究,是数学推理过程的机械化以至自动化,尽量减少对聪明才智的要求,并由此减轻艰难的重脑力劳动。数学机械化实现的关键在于寻找某些依据和法则可以机械按部就班进行的方法

6、,在现代通常称为算法,而这种算法又可以编写成程序在计算机上实施。数学机械化就是数学定理能够在计算机上实现证明。定理的机器证明是指使用计算机证明定理成立,即把人工证明定理的过程,通过一套符号体系加以形式化,变成一系列在计算机上自动实现的符号计算推导过程,它的实质是把具有智能特点的推理演绎过程机械化。定理的机器证明是人工智能领域一个重要的分支,从传统手工证明到定理机器证明的转变是现代数学思想方法的一次重大突破。机械化思想早在我国古代数学就已经存在了。中国古代数学主要以算筹为运算工具,从汉初完成的九章算术中对开平方、开立方机械化过程的描述,到宋元时代发展起来的求解高次代数方程组的机械化方法,无一不与

7、数学机械化思想息息相关。在近代,机械方法证明数学定理的思想是从世纪法国数学家笛卡尔创立的解析几何开始的。解析几何的创立,第一次将无章可循的几何定理证明按一定的步骤化为代数形式解决,在空间形式和数量关系之间架起了一座理论桥梁,为几何问题的证明方法走上机械化道路奠定了基础。德国著名数理逻辑学家、微积分学创始人莱布尼兹明确提出机器可成为推理工具的思想,他制造了最原始的乘法计算器,并设想研制“推理机器能够自动检验数学命题的正确性。世纪末,德国数学家希尔伯特埘从理论上提出定理证明机械化的思想。年函数的微分、偏微分及梯度、散度、旋度在语言下的实现他在经典名著几何基础一书中叙述了数学机械化定理:“初等几何中

8、只涉及从属于平行关系的定理证明可以机械化。这个定理提供了一条从公理化出发,通过代数化而达到机械化的道路,至此数学证明的机械化思想初步形成。但这些思想在当时仅仅是一种预示性的理论,无法在实际中具体操作实施。世纪年代电子计算机问世为数学定理的机器证明提供了物质设备条件,使数学机械化思想有了实现的可能性。年代中期,美国开始了利用计算机证明数学定理的尝试。年,美国卡尔基大学一兰德公司协作组的纽厄尔八、西蒙.和肖乌等人建立了机器证明的启发式搜索法,编成了一个“逻辑理论机程序,成功证明了罗素、怀特海所著的数学原理第二章条定理中的条定理,是机器证明史上第一个奠基性的突破,这一年可作为人类历史上计算机证明的开

9、端。年,著名数学逻辑学家、美籍华人王浩教授设计了一个机械化方法,在机上仅用分钟的运行时间证明了数学原理这一经典著作中的几百条定理,在数学和数理逻辑学界引起了轰动,宣告了数学定理计算机证明操作的可行性。年美国的阿佩尔、哈肯和科奇完成了构造可约构形的不可避免集工作,在高速计算机上用近小时证明了“四色问题德国数学家麦比乌斯于年提出著名的四色猜想:“如果只用四种颜色能否对球面上或平面上的任何地图着色”,使一百多年来未悬而未决的难题得到解决,震惊了学术界。这一事件表明计算机作为辅助工具在定理证明中存在着巨大的潜力。我国也于世纪年代参与到数学机械化这个新兴研究领域中。年著名数学家吴文俊院士在中国科学上发表

10、初等几何判定问题与机械化证明的科学论文,提出了用计算机证明几何定理的机械化方法。它与通常基于数理逻辑的证明方法有着本质的不同,显现了无比的优越性,第一次在计算机上证明了一大类初等几何问题,如西姆松定理、弗尔巴哈定理、莫勒定理等,还发现了不少新的不平凡几何定理,实现了初等几何与微分几何定理的机器证明,开创了一个崭新的数学机械化领域。.国内外研究现状在当今的信息时代,随着数学机械化研究的不断深入,人们已经能够根据机械化方法创建各种机器语言来编写程序,并在计算机上给出证明。短短几十年内,人们不仅对初等几何和微分几何中的一些主要定理的证明实现了机械化,近年来又对三角函数、双曲函数等一类超越函数的公式实

11、现了机械化证明。同时机器证明在分析拓扑学、集合论以及递归函数等方面都获得了成功的应用。数学机械化青岛科技人学研究生学位论文不仅仅是数学本身理论研究方面的实质性进展,也为诸多高科技问题的解决提供有力的工具。它不断发展到众多前沿领域,用于解决计算机图形与视觉、信息处理、数控技术中的关键问题,建立自动推理平台,而且被应用于如力学、理论物理、数控机床、计算机辅助设计等交叉学科。迄今为止,全世界已存在种可用来进行定理证明的机器语言系统,其中有种数学定理证明系统受到北美数学知识管理组织简称,致力于数学机械化的一个国际化的数学组织及大多数专家的认可,譬如系统、系统、系统,和系统。近年来,越来越受人们关注的还

12、有和。荷兰数学家从是否需要数学数据知识库 支持这个方面对、/、/、/、等种著名的数学定理证明系统进行比较,发现、/、等个系统需要庞大的数学数据知识库支持。至今为止,系统拥有世界上最大的数学领域知识库。在国内,以吴文俊院士为首的数学家们坚持不懈地从事几何定理证明机械化的研究,形成了自动推理的中国学派,使我国在数学机械化领域处于国际领先地位。年,张景中院士根据面积法创立消点算法,成功地研制出几何定理自动生成的可读数学证明的软件。年,张景中、杨路、高小山、周咸青合作实现了第一个非欧几何定理证明自动生成的算法和程序,迅即产生了一百多个非欧几何定理的可读证明,其中半数以上的定理是从未见过或未被证明的。年

13、,杨路创立了降维算法并研制出实现这种算法的数学软件,在计算机上实现了二千多个不等式的机械化证明,是几何定理机械化证明领域的又一个重大突破。年张景中院士研制出第三代智能数学平台软件,它的推广有利于加快中学数学现代化进程,开创了世界智能性数学教学软件的先河。我国数学家开拓的新的数学机械化道路,在国际上产生了巨大的影响。宣言向人们描绘了未来的数学世界:“将来所有的数学知识都可以用计算机以编码的形式编写,并通过机器进行验证和改错。人们的这个梦想完全体现在当今世界层出不穷的各种定理证明系统中。.系统的发展历史和研究现状系统是从人工智能的一个分支?定理自动证明的发展过程中产生和函数的微分、偏微分及梯度、散

14、度、旋度在语言下的实现发展起来的,用于构建数学知识库的证明校验的计算机语言系统,是一个数学定理证明工具。如今已发展成为集逻辑证明、推理演绎、复杂计算、校验排版功能于一体的数学信息处理的形式化系统,并拥有自己的编辑语言?语言和世界上最大的数学数据知识库。起源于年,当时正在撰写拓扑学博士论文拘 教授萌生了一种强烈的想法一能否借助计算机撰写自己的数学论文。在年月日召开的华沙大学图书馆学和科学信息学院的研讨会上, 教授第一次提出要创建开发一种可以用来帮助撰写数学论文的计算机语言,论证了实现的可行性,并对这种语言在功能上具备的一些特点作了说明:、具有可存储性和可编译性,撰写的论文可存储在计算机中,并且可

15、将其翻译成数学语言;、格式整齐,语法简洁易懂;、具有支撑整个数学领域自动化信息系统的基本要素;、具备简便查验错误、查证参考文献、删减重复定理的功能;、具备实现自动排版的功能;、可进行数学定理证明的相关教学活动。和第一个可运行的系统是 ,教授于年秋天合作设计的关于逻辑谓词验算的语言程序,并在系统的计算机上成功运行。虽然耗时较长,但语法分析和语义结构是完全正确的。年月, 教授发表了一篇名为“的短文,第一次以文字的形式论述了他创建的机器证明语言?语言。随即语言的研究得到波兰科学协会的资金支持,同年月,教授向该协会提交了语言的初级版本:.,同时介绍了如何使用语言借助雅斯科夫斯基自然演绎推理方法撰写逻辑

16、谓词验算的证明过程,值得一提的是当时教授预见数学知识数据库的问题。此时的系统已经可以用地?、?、?虹?、丛?、?.。这样的语义词来编写定理证明的过程了。.年间,在华沙大学被用于谓词逻辑及数学命题计算机辅助证明课程的教学中。年,系统实现了至/ 的艰难进化,并完成了将系统发展成为./的目标。年,系统在语义和句法方面做了大量的充实和改进,新定义了谓词、结构、预声明、绝对相等 等概念,并首次对关系和函数进行了定义,系统升级为青岛科技人学研究生学位论文,很多命题已不需要证明就能在系统中实现自行验证。年年间,系统完成了从.到讫.的升级,首次在论文中出现了对环境部的设置,文章格式更加规范。系统在、和等多种不

17、同的机器上的成功运行,充分的说明了语法的正确性及逻辑的合理性。在?年和年,分别实现了和.两次重大的突破,现在所用的版本就是从再次升级的系统演化而来的。.年是系统实现飞跃发展的重要时期。年,应用在机上的成功运行,被称为.。次年月日,数学数据库?正式开始使用。月日,第一篇标准的.论文教授将讫系统中加入。上蔓癸,大收录于中。月到月间,大增强了文章的可读性。年,基于系统的论文期刊正式出版发行。.年间,期刊得到了美国的资金支持。年,协会的教授在系统中增加了用于查询语义的浏览工具。年,数学百科全书 完成。经过多年的发展,系统目前已升级到.版本,.数据库中收录的文章达一千余篇,包含了万多个数学定义,多万条定

18、理。.课题研究的目的和意义以自然演绎推理的古典逻辑为基本框架,从逻辑推理和数学定理证明发展起来的系统,具有撰写和检验数学论文的双重功能。目前,诸多数学领域,如集合论、代数学、分析学、拓扑学、运筹学中的绝大多数定理都可以利用系统进行证明,很多复杂的数学定理实现了机械化证明,一些难以证实的猜想得到了初步证明,并且发现了一批新定理。同时,系统也在不断实现自我完善与发展,提升了语言的处理能力,扩充了的知识储备,系统的自动逻辑推理和校验纠错的能力得到加强,加速了与其他机器证明工具的交叉研究和相互转化。此外,系统具有智能性的“人机对话”功能,在推理演绎过程中能自动发现论证的矛盾性,提高了使用系统的安全性和

19、科学性。除了自身的发展外,系统还为数学机械化和其他领域的机械化研究提供可行的新思路、新方法、新工具。日本的数学家、计算机科学专家 函数的微分、偏微分及梯度、散度、旋度在语言下的实现教授,利用语言完成抽线定理的证明,并且在人工智能方面使系统参与实现了微型机器人、音像识别系统、自动化控制、数字信号传输等多方面的成果研究。将来随着计算机的飞速发展和研究的不断深入,系统势必在更多领域得到广泛应用。. 课题研究的主要内容系统自年建立以来,数据库不断充实完善,系统完成了数次成功的升级,收录了来自波兰、日本、中国、加拿大等多个国家的教授学者和研究生撰写的数学论文。几乎含盖了数学领域的所有学科,如数学分析、集

20、合论、代数学、几何学、拓扑学、逻辑学、图论、范畴理论等等。微分学的出现,为人们研究各种运动提供了犀利的数学工具。诚如恩格斯所说:“只有微分学才能使自然科学有可能用数学来不仅仅表明状态,而且也表明过程?运动。实际上当今微分学的运用不单单局限在自然过程,它已被延伸到微分方程、向量分析、变分法、复分析、时域微分和微分拓扑等领域。偏微分作为微分学的一个重要分支,与其他数学分支有着广泛的联系,如在广义函数与空间、椭圆边值问题、能量方法、算子半群等方面。同时偏微分在工程技术中也有广泛的应用,建筑、航空航天等现代技术中都以其作为基本的数学工具。虽然数学库知识储备庞大,但关于多元函数高阶偏微分理论及梯度、散度

21、、旋度的定义和相关性质等都没有涉及和实现。本课题的研究是建立在对数学定理的机器证明和数学定理的自动推理系统?娩及其语义、语法深刻理解的基础上,在系统中利用系统语言和庞大的数学数据库,对函数偏微分及梯度、散度、旋度的理论和方法做进一步研究。借助对系统和数学机械化的探讨,为后继的高维微积分基本定理及梯度、散度、旋度同外微分算子的理论等方面在系统下实现机械化奠定理论和实践基础。本文主要从以下几个方面在系统中进行研究:.基于中对于函数微分和赋泛线性空间中函数偏微分的一般性定义,给出借助单变量函数微分为依托而建立起来的欧氏空间中二元函数偏微分定义的新形式,在此基础上进而讨论了二元函数偏微分的运算性质以及

22、可微与连续的关系。.在系统下,从另一个角度将欧氏空间中二元函数的二阶微分看作二元函数偏微分的再次微分进行定义,首次实现了二阶偏微分的叙述。定义的形式简洁明了,与之前给出的二元函数偏微分的定义保持了形式上的一致性,并青岛科技人学研究生学位论文给出相应的公式和相关定理的证明。.将二元函数偏微分的定义和定理推广到三维欧氏空间中,利用逻辑语言给出了矢量场的表示形式,由此在下第一次定义了在近代物理学、高阶椭圆方程、高阶抛物方程、方程等偏微分方程中应用广泛的梯度、散度、旋度并将彼此间的关系实现了机械化。本文围绕着多元函数的偏微分内容展开,主要讨论了欧氏空间中二元、三元函数的偏微分、高阶偏微分的相关定理以及

23、梯度、散度、旋度等内容,均在系统中得以实现。创新之处是在系统中首次定义了函数微分学中诸多概念和偏微分算子表达式,建立了一个关于函数偏微分学较为完整的理论体系,实现了定理的证明,系统地完成了数学理论的转化。函数的微分、偏微分及梯度、散度、旋度在语言下的实现系统概述.系统简介系统由波兰华沙大学的 教授组织拘协会领导,其逻辑框架基于自然演绎推理的古典逻辑。系统的建立的起始目的是设计一个软件环境来帮助数学家处理、撰写和验证数学论文,因此古典数学和集合理论就成为软件环境发展的基础。系统主要由三部分组成:.语言。帮助数学家使用计算机可以识别的语言撰写数学学术论文。.软件。用于整理编排数学学术论文和检验其正

24、确性与否。.数据库。是世界上可以被计算机检验和处理的最大的数学知识数据库。使用语言进行定义、计算、推理演绎及数学定理证明而形成的文章称为文章,利用系统提供的软件可以在计算机上对其进行检验和优化。通过系统验证准确无误的论文将被发表在波兰的 杂志上,并收录至数学数据库中。.语言.语言是数学逻辑推理演绎的计算机语言,由包含数字、英文字母和各类标号在内的码组成,这些基本的符号是依据常用的数学符号与一般的码相结合的原则定义出来的,是计算机可以编译、人类可以识别的一种程序化语言。该语言的逻辑符号是在纯粹的数学符号及其英文表述和一般的字符相结合的基础上演变发展起来的。表?对普通数学命题中的逻辑符号和语言中的

25、逻辑符号进行了比较:、? ? : ,普通数学命题中一的逻辑符号 语言中 八 /的逻辑符号表普通数学命题中的逻辑符号和语言系统中的逻辑符号青岛科技大学研究生学位论文在语言系统中,每一个变量都有自己从属的数据类型。在书写文章时必须声明所使用的变量是数据库中的哪一种数据类型,以便系统处理文章。若不进行变量声明,系统将不承认其存在的合理性。主要包含以下几种数据类型:集合,自然数,实数,复数,拓扑空间,矩阵,实数集,复数集,的子集等等。.文章结构数据库中的文章,都是使用语言撰写的。文章是文本文件,可以在任何一个文本编辑软件中编写。文章包括两部分:环境部和文章的主体部分 。具体形式见图?所示:图 缸文章的

26、一般结构:.?在部分,要对论文书写过程中引用的定义、定理、符号和结构等的出处进行声明,相当于普通数学论文中的参考文献部分。环境部具体可以分为五部分:词汇引用,符号引用,包括:,定义引用,定理引用,模式引用。图?说明了的书写格式:函数的微分、偏微分及梯度、散度、旋度在语言下的实现图环境部引用分类词汇远. 其中,.县,:,.月。表示被引用的文章名列表。部分是文章引用的词汇列表,同时也表明了算符词汇的运算优先级。部分包括,通知处理器这篇文章可以使用此处列出的文章里的符号。其他三个引用,表明论文可以引用这些列表文章中的定义、定理、模式等。文章的主体部分包括作者所作的数学术语、定义及与定义相关的性质,见

27、图.。通过定义新概念,编写逻辑证明,列举特例,完成定理的演绎,从而实现理论体系的转化,使数学理论得以在系统中继续发展。青岛科技大学研究生学位论文馘图.文部分的内容组成.?.基本命题表述词汇常用于命题表述的语言词汇和基本的语法句型有:数据属性预声明、结构词和、假设词、简单依据引导词、结构依据引导词、推导词、“任意取定词、“存在取定词、因果连接词、结论引导词和、条件引导词和、存在条件引导词、全称命题?、扩散陈述命题?、数据属性转换?硒?等等。论文就是由这些语言词汇和语法句型连接的命题表述或证明。语法逻辑也蕴含在如数学归纳法、分类讨论法、同一性证明方法、归谬法等各种具体方法中,在欧氏空间中偏微分、高

28、阶偏微分和矢量场实现的章节中,我们将给出具体示例和详细说明。.中定理证明的方法系统是基于§演绎推理的古典逻辑构建而成的,拥有符合古典逻辑推理的基本证明方法。. 语言中命题表述的一般形式与传统数学语言陈述命题类似,语言中主要有七种命题表述:、简单命题【】,、与命题】&【,函数的微分、偏微分及梯度、散度、旋度在语言下的实现【】,、推导命题】、等价命题【】 【】、或命题】 【】,、全称命题 “】,【】。、存在命题这里的【】和【】分别代表关于,的命题。.基本证明方法、直接法从命题条件出发,通过正确合理的推导过程得出命题的结论。举例:用直接法证明命题“若,则; :为命题条件; :为命题

29、结论,得证成立;、间接法又称反证法或无理法,即假设命题结论的否命题成立,通过推导得出矛盾。“是使用是间接法的标志。举例:用间接法证明命题“若,则;勰 ; :假设非成立,即假设命题结论的否命题成立;:推得矛盾,说明与非不能同时成立;、特殊命题的证明方法与命题拆分证明法拆分法即将命题拆成多个分命题,通过对分命题逐个证明,来完成命题整体的证明。青岛科技入学研究生学位论文等价命题双向法双向法即将等价命题看作“左推右”和“右推左两个方向的单命题,再依次采用直接法或间接法进行推理证明。或命题单一否定法或反证法通常采用单一否定法,即通过否定其中一个命题,完成肯定另一个命题的证明。也可以用反证法,即将命题的结

30、论全部否定,通过推理得出矛盾,从而证明必有或命题中的一个结论成立。扩散性命题的证明方法通常采用以“?为引导词的语句证明。.存在性命题的证明一般用“?”语句作总结性证明。.系统中的定义在系统中,对定义的要求十分严格,不但定义本身要缜密合理,而且分类要明确。泣系统的定义主要包括:模式定义、谓词定义、算子定、属性定义、定义、结构定义。对于不同类型的定义是否需要证明存在性和唯一性系统做出了明确的规定,如表中所示【】,“表示需要证明,无“表示无需证明。模式 谓词算子 属性表定义证明分类.模式定义“”是模式定义的标志,有两种定义的形式,分别由和来引导。形式的定义需要证明存在性,形式的定义不需证明。举例:?

31、、; ,】;函数的微分、偏微分及梯度、散度、旋度在语言下的实现、; ?,.;.谓词定义.谓词的定义可以理解为定义一种表达性叙述的数学语句,如定义是的因子,表达“某数是某数的因子的数学语句就是谓词。一般地,在语句中,“是谓词定义的标志。定义的格式如下:;?. 宰;.算子定义算子的定义,可以看作是定义一个新的函数,规定由陈述性语言定义的新算子必须证明存在性和唯一性,否则系统软件校验时不承认定义方式的合理性,“”和“”是算子定义的标志。举例:,;.,】 ;:这个与对应;在中,如果由已存在的函数算子或数值运算来定义新算子,无须证明存在性和唯一性,只需证明一致性,这种定义方式以“为标志。, /;】青岛科

32、技大学研究生学位论文:定义的算子由已存在算子、相除得到,因此在定义过程中只需证明。;.属性定义属性的定义,是对数学特性的一种描述性说明,以“”为标志。如果讨论的某个数据满足后面的性质,便说明它具有这种属性。举例:; ?& ;上面的属性定义表明收敛到的自然序列具有“不为零、“本身收敛、“取极限为零这三个属性。.定义定义的实质也是一种声明,通常有两种含义:一是对某种模式赋予某种属性,从而复合为一个新的模式,要求对存在性给予证明;二是声明两种模式间的隶属关系,要对一致性给予证明。两种含义的示例如下:、; ;:对“这种属性的定义;:;为新定义的。上例对模式“”赋予“”属性,且、一 ;:隶属于;

33、函数的微分、偏微分及梯度、散度、旋度在语言下的实现.结构定.结构的定义,通常伴随新函子拘定义,:支撑起整个结构,并且对的数量和属性类型是没有限制的。“是结构定义的标志,其定义的一般格式为:够%一届,口殷,?“,。一成彬;其中,是新定义的结构名,%,?,%是函子名,层,尾,?,凤是函子对应的属性类型。.重新定义重新定义是指对数据库中已存在的定义,在不改变原定义符号的前提下,改变定义的数据属性或定义本身的表述内容而重新对定义作出的一种声明。对于前者,需要证明重新定义与原定义之间的一致性;而后者需要证明前后两个定义具有兼容性。重新定义以“为标志。举例:、,;,;,;:,佗:,【:,:】;、; ; ;

34、青岛科技人学研究生学位论文二元函数偏微分勺实现微分学作为变量数学的开端,它的创立极大推动了数学的发展,过去很多初等数学束手无策的问题,运用微分学,往往迎刃而解,显示出其非凡威力。而偏微分作为微分学的一个重要分支,与其他数学分支如椭圆边值问题、广义函数与空间、算子半群、能量方法等都有着广泛的联系,并且在自然科学与工程技术中有着广泛的实际应用。在数据库中,一元函数微分的理论已经基本完备,有关赋范线性空间中抽象意义上的偏微分内容也有涉及,但缺少欧氏空间中应用最广的实二元函数偏微分的实现,关于二元函数偏微分具体的系统理论也少有论述。本章主要介绍如何将上述内容在系统中实现并通过系统的校验。.二元函数偏微

35、分的基本知识本节就多元函数微分学中有关二元函数偏微分的定义和性质做一些介绍。定义.【】设函数厂,在点昂,的某邻域醐岛内有定义,对于中的点如力,若函数在点昂处的全增量垃可表示为:办一媾,奶.“力其中曰是仅与点昂有关的常数,夕妒匈,力是较户高阶的无穷小量,则称函数厂在点昂可微。并称.式中关于昀每的线性函数为函数,在点昂的全微分,记作.出,由.、.可见出是的线性主部,特别当叫,纠充分小时,全微分函数的微分、偏微分及梯度、散度、旋度在语言下的实现龙可作为全增量垃的近似值,即.,似,斜,一而?二元函数当固定其中的一个自变量时,它对另一个自变量的导数称为偏导数。于是,偏微分的定义如下:定义.【】设函数,。

36、若%,。,且厂%在而某一邻域内有定义,则当极限。硫垒亟:塑 :缸?帕缸卅 存在时,称这个极限为函数厂在点,关于的偏导数,记作,或可,蜘。同理,可得到厂在点%,%关于的偏导数的定义。若函数,在区域上的每一点,都存在对或对少的偏导数,则得到函数厂,在区域上对或对的偏导函数,记作正,或,胁或二元函数,的几何图像通常是三维空间中的曲面。设,为这曲面上一点,其中,过昂作平面,一,它与曲面的交线:二麓,是平面?上的一条曲线。二元函数偏导数的几何意义是:,作为一元函数厂%在一而的导数,就是曲线在点昂处的切线对轴的斜率,即切线与轴正向所成倾角的正切值。同样,是平面而与曲面,似的交线青岛科技大学研究生学位论文:

37、嚣,在点昂处的切线关于少轴的斜率。.二元函数偏微分的实现及其性质的论证系统的两大灵魂支柱:一是通用语言;二是推理验证程序。前者摒除了日常语言表述数学的不规则性、繁杂性,它使用简单明了的符号、合理的语法规则,使得逻辑推理和演绎易于进行。后者则用作推理检验的工具,它处理利用语言撰写的推理演绎程序,从而使逻辑演算按照一条明确的道路进行下去。利用系统进行数学定理的证明有两个鲜明特点:算法化,遵循了一定的语句规则和书写程序;刻板化,所有的论证步骤都是根据一定的法则按部就班地进行,不能存在间断性和跳跃性。基于以上考虑因素,为达到利用语言实现有关函数偏微分的论证,首要的工作就是将偏微分的定义形式化,这种定义

38、既要求区别于数据库中已存在的微分定义,还要与微分定义建立联系便于系统识别。在偏微分定义形式化的基础上进而讨论相关的定理和性质。.环境部的设置和变量的声明首先,根据论文内容对环境部进行初步的设置。,:门, , , , ,研二,一,一,一,;,一,一, ,了,;, , ,腑二, ,瞳,函数的微分、偏微分及梯度、散度、旋度在语言下的实现玳;,一,.,;,;,一,;, , ,瞳, ,;以上是对环境部的初始设置,但这并不是最终的形式。因为在论文起始撰写阶段,不能确定环境部列举的文章是否完全需要引用,随着文章的深入展开,也会有新引用的文章添加,在最后论文优化过程中也需要删除没被引用的文章,所以说刚开始建立

39、的环境部不是完全固定的。由于本文有新定义的内容,在环境部的需要添加本文的文章名 ,便于系统识别、检测。随后声明文章中使用的变量的数据类型:;, ;,冱,】【, , ; , ; , ,;,;,., ;.二元函数偏微分的表述在预备知识中,约定,。,为实数,为二维欧氏空间中的点,为二维欧氏空间尺中的子集,厂,五,厶为尺到尺拘,为收敛至零的实序列,三是线性函数。青岛科技大学研究生学位论文一:, ,一;, ,.鼍,三:一:。 ,。,.,一;以第一个定理为例,“:,后的“肼:”表示此定理被收录于数学数据库文章 :和定理.中,是该文章的第个定理。定理:说明了函数叫,啊,的定义域和值域均为实数集尺,对二维。欧

40、氏空间中的任一点,都有:.,和,.石,在一元函数微分学中,若厂力在点而可微,在函数的增量厂而曲一厂一其中?,%。由.论述可知,若二元函数,在一而,%可微,则厂在一%,处的全增量可由厂而力缸表示。有时也把上式写成如下形式.础这里口一。,如?四,如?鹊在.式中令缈缸,这时得到应关于的偏增量,且有印尬池或苦口现让血专,由上式便得的一个极限表达式。彳:生:.缸 缸珈容易看出,.式右边的极限正是关于的一元函数,似%在戈而处的导数。类似地,令,由.式又可得到函数的微分、偏微分及梯度、散度、旋度在语言下的实现。:生:.晦诚趣瑚晦 坶它是关于的一元函数厂,力在处的导数。在数学数据库中已存在关于一元函数的微分的

41、定义,通过以上分析,我们考虑能否定义单变量函数,对应着当二元函数固定其中一个变量时得到的函数厂似或厂,力如果这种想法在系统中可以实现的话,那么二元函数的偏微分就可以借助单变量函数的微分进行定义,而且能与中关于一元函数微分理论在形式上保持很好的一致性。于是,在系统中我们定义两个单变量函数.咧厂,力,.吼歹厂,力,具体如下:,;,苎坚】圣一 一:,;。苎坚至三一 :一:,:;其中巩,.吼霉厂,力是新定义的函数名,“.后面是对应函数的属性类型。在中函数如下定义:;, :&.,;对于二维欧氏空间的点似力可以看作实数序列,函数在自变量取的函数值是把序列的第一个元素替换成,而得到的新序列,.,即:

42、.,力。一:,两个函数复合得到的,函数删厂,是由呻砰和青岛科技人学研究生学位论文这样定义的删,力实质上就是专的单变量函数以似力的第一个分量为自变量,由于在定义形式为,即用已存在的数值运算定义新的算子,无需证明新算子的存在性和唯一性,只需证明一致性见.,。吼厂,的定义同理。关于单变量函数的定义经过系统的翻译软件翻译之后,其一般性表述为: 冗 :冗.,我聚猫, :跏 ,慧,?,嚣. 凌鏊 磁缎, :,露,?,名.借助以上两个单变量函数的定义,给出二元函数偏微分在下的谓词定义:,;:, ,;,?:酊丽百五面.再石聂三一弋赢可丽两;。? ;定义谓词“ 、”和“.义是,二元函数,在第一个变量而处存在偏微

43、分即单变量函数删,在而处可微,在第二个变量%处存在偏微分即单变量函数汗,力在%处可微,这样的谓词语句达到了对二元函数偏微分的定义可以借助一元函数可微定义表述的目的,并证明有下列定理成立:一:一量 ,?一 。,.?,.。.?.?:、的含函数的微分、偏微分及梯度、散度、旋度在语言下的实现一:一日,.一。.一日?.?;收录在中的 .已经对一元函数可微性作出如下的原始谓词定. ;: : ,.?.?;系统对谓词的定义形式往往是开放性的,不拘于某一固定形式,为了应用定义便于进行定理证明,我们将二元函数偏微分的定义做进一步修正,用重新定义:。:。 : : , 鼍, ,毛。,.?,.?.?;。: : : ,

44、一。日鼍, 。,.一,.一.,一;: :将矸: 和 , 比较可以看出,通过:重新定义的谓词 , : 在形式上和数据库已有定义:更好地保持了统一性,使得数据库中大量使用微分原始定义推证的定理也可以借鉴应用到偏微分定理的推导中,大大降低了推理复杂繁琐化程度。重新定义二元函数的偏微分,改变了谓词本身的表述内容,要证明前后两个青岛科技人学研究生学位论文中在定义具有兼容性见.。以册乙:下的证明过程举例说明,具体如下:,。 ;: : , 量, 。,.?.?日?.?.前而币丁弋开可两了百可.?: ;日,:;量日,。 , 日? ?,.?,.日.?.?:, ; :;:;董日, , ,.?,.?口.?,:, ,.

45、?,.?.? ;,。? ,一:耳,监;.、可在正时,一方面要证明由“ .推得“ 幸 木, ,;& ., .?.?”;另一方面假设?在条件“木,?& ,&函数的微分、偏微分及梯度、散度、旋度在语言下的实现.?.”成立的基础、 上,推证“ 。只有两个方面都给出证明,才能保正得证。从上述定理证明中可以看出,对于一个命题完整的“论述一判定一证明过程必须建立在牢固的逻辑推理基础上,也就是谓词演算,每一个步骤的推导都要有严格的依据由引导理论依据:可以是定理中假设语句,如;可以是已证明的语句或定义,如:,;也可以是引用中已存在的:定义或定理,如 。这就是系统利用数理逻辑强调形式化和严

46、格化的想法,从而达到利用计算机证明数学定理的最终目的。:定义中的同理可证。中 .关于赋范线形空间中抽象意义上函数偏微分的表述为:;,;,;? :,.;:在中,厂:尺“呻尺的,对于彤中的点,在点的第个分量的偏微分定义为“, ,.”。定理 :和 :说明了本文定义的偏微分和 在谓词形式上的充分必要性。一:,?一。?.一:,量堑?一。;?噫为“当且仅当”,是等价命题的表述的标志,旨在说明两种谓词定义表述的充要性。新定义的二元函数偏微分及定理在期刊中的一般表述为:青岛科技大学研究生学位论文笼咒., 。, 撒 . ,名慧, /,名。 篙 :辫 . ,/髫黜, 名洳. : 之.名篇。洳 .。,霓黼,名一名铷

47、端?嚣一黝. 。 名怒,蜘疆。等叛筑.露 伪嘴暑, ,芗一名蜘嚣一翔一洳.奢之 致 名疆 奢己. , . 腿. ,蜘名黛翔。铷。冬.三, 若,一,铷?十一勘.冗,魏秘 踅.璐。搬; 名,喇. . ,细 茹踟,鳓. 名.踅.芒名驴一,名蜘一蜘十磁碧一翔. :冠 凌 动厂 冗。; 名 歹 .。., 冗协凌孑冗。弧歹魄。.函数的微分、偏微分及梯度、散度、旋度在语言下的实现通过上面的分析可以看出,语言虽然是一门计算机语言,但它非常接近人类处理数学问题的自然语言。利用它在计算机上证明,与人用笔在纸上书写的证明存在很大的相通性。这种证明不再是过去那种计算机能够识别而人看不明白的证明,而是人和计算机都能读得

48、懂看得明白的证明,是使计算机能像处理算术一样处理数学问题这条探究道路上的一个伟大的里程碑。完成了二元函数偏微分的谓词定义,下面是在算子的层面上进行定义,使得二元函数的偏微分可以进行运算和相关性质的讨论。,: :一:,一 ,;:定义的两个偏微分算子表达式为,它们的数据类型为实数,在数值上等于,。在这个定义中,“通过软件检测是默认成立的,故无需再进行证明,但依循证明严密性要求,在定义过程中“”语句是不能省略的。同样地,为了保持与一元函数微分算子的一致性,我们给出二元函数偏微分算子的另一种定义形式,并将其转换成相应的定理。:量日,日羹 ;。, 鼍。口 ,.,。.?,.?.?:日, ,日 鼍,。,., ,.一,.日.一?.?日;青岛科技大学研究生学位论文:一:量日, 。?、一