（应用数学专业论文）向量函数、微分及偏微分基本公式的计算机证明.pdf

青岛科技大学研究生学位论文 向量函数、微分及偏微分基本公式的计算机证明 摘要 m i z a r 系统是由波兰华沙大学的a n d r z e jt r y b u l e c 教授于二十世纪七十年代开 创的集逻辑证明、推理演绎、校验排版、复杂计算、科研教学功能于一体的形式 化系统，同时在自动化控制、声音和图像识别等研究领域有着广泛的应用。如今 该系统拥有世界上最大的数据库m m l 。 本文首先介绍m i z a r 系统的发展历史，其次简要说明m i z a l - 论文的基本结构。 利用m i z a r 语言系统实现了向量函数的表示，讨论其若干性质。给出向量函数微 分及偏微分算子的定义，并在计算机上推导证明了若干基本公式。 本文主要从以下几个方面在m i z a r 系统中进行研究： 1 基于m i z a r 中对于度量空间和欧氏空间定义的理解，给出了向量函数的 m j z a r 表示，在此基础上进而讨论了向量函数的有关性质。 2 在1 v l i z a r 系统下，借助实函数可微性的定义，给出向量函数微分定义的 m j z a r 形式，并证明了向量函数微分的基本公式。 3 利用m i z a r 系统中1 1 维赋范线性空间的偏微分算子定义，实现了向量函数 偏微分的定义，并完成了向量函数偏微分的基本公式的形式化表示。 以上结果均通过了m j z a t 系统的验证，并以论文形式发表在f o r m a l i z e d m a t h e m a t i c s 杂志上。 关键词：数学形式化m i z a r 语言系统向量函数微分偏微分 青岛科技人学研究乍学位论文 c o m p u t e rp r o v i n go f b a s i cf o r m u l a si nv e c t o r f u n c t i o n d i f f e r e n t i a la n dp a r t i a l d i f f e r e n t i a t l 0 n a b s t r a c t m i z a rs y s t e ma saf o r m a l i z e ds y s t e mi si n i t i a t e d b yt h ep r o f e s s o ra n d r z e j t r y b u l e co fw a r s a wu n i v e r s i t y ( p o l a n d ) i nt h e19 7 0 s ，w i t ht h ef u n c t i o no fl o g i c a l p r o o f , a u t o m a t e dr e a s o n i n g ，v e r i f y i n ga n dt y p e s e t t i n g ，c o m p l e xc o m p u t a t i o na n d s c i e n t i f i cr e s e a r c ha n dt e a c h i n g a tt h es a m et i m e ，i t sw i d e l yu s e di nr e s e a r c ha r e a s s u c ha sa u t o m a t i o nc o n t r o l ，v o i c er e c o g n i t i o na n di m a g er e c o g n i t i o n n o w a d a y s ，t h e s y s t e mh a st h ew o r l d sl a r g e s td a t a b a s em m l t h i sp a p e rf i r s t l yi n t r o d u c e st h eh i s t o r yo fm i z a rs y s t e m ，t h e nd e s c r i b e st h eb a s i c s t r u c t u r eo fm i z a ra r t i c l e s v e c t o rf u n c t i o ni sp r e s e n t e da n di t sp r o p e r t i e sa r ed i s c u s s e d t h r o u g h t h em i z a rl a n g u a g e s y s t e m v e c t o rf u n c t i o nd i f f e r e n t i a l a n d p a r t i a l d i f f e r e n t i a t i o no p e r a t o r sa r ed e f i n e da n dt h e i rr e l a t e db a s i cf o r m u l a sa r ed e r i v e da n d p r o v e d t h em a i nw o r ko f t h i sp a p e ri sa sf o l l o w s ： 。 1 v e c t o rf u n c t i o n sm i z a rd e n o t a t i o ni sg i v e ni nt h eb a s i so fd e f i n i t i o n so fm e t r i c s p a c ea n de u c l i d e a ns p a c ea n di t sp r o p e r t i e sa r ed i s c u s s e d 2 d i f f e r e n t i a l sm i z a rf o r mo fv e c t o rf u n c t i o ni sg i v e nb yd i n to ft h ed e f i n i t i o no f r e a lf u n c t i o nd i f f e r e n t i a b i l i t y t h e nt h e i rb a s i cf o r m u l a sa r ep r o v e d 3 m a k i n gu s eo fp a r t i a ld i f f e r e n t i a t i o no p e r a t o ro nn o r m e dl i n e a rs p a c e sr ”i n m i z a rs y s t e m ，p a r t i a ld i f f e r e n t i a t i o n sd e f i n i t i o no fv e c t o rf u n c t i o ni sr e a l i z e d a n d m i z a rf o r m so fc o r r e l a t i v ef o r m u l a sa r ed e r i v e d t h e s er e s u l t sa r ev e r i f i e dt ob ec o r r e c tb ym i z a rs y s t e ma n dp u b l i s h e di n f o r m a l i z e dm a t h e m a t i c si nt h ef o r mo fp a p e r k e yw o r d s ：m a t h e m a t i c sf o r m a l i z a t i o n ，m i z a rl a n g u a g es y s t e m ，v e c t o rf u n c t i o n ， d i f f e r e n t i a l ，p a r t i a ld e f f e r e n t i a t i o n 青岛科技人学研究乍学何论文 目录 中文摘要l 英文摘要l i 1 绪论1 1 1m i z a r 系统的发展历史l 1 2m i z a r 论文简介3 1 2 1 论文结构3 1 2 2 环境部3 1 2 3 正文部分4 1 2 4 语言的综合使用4 1 3 课题研究的主要内容5 1 4 课题研究的目的和意义5 2 向量函数的m i z a r 实现7 2 1 预备知识7 2 2 向量函数定义的m i z a r 实现及其性质的证明8 2 2 1 环境部的设置和变量的声明8 2 2 2 向量函数定义的m i z a r 实现9 2 2 3 向量函数有关性质的m i z a r t i e 明一1 1 2 2 4 向量函数有关命题的m i z a r 表述1 5 3 向量函数微分的计算机证明1 7 3 1 预备知识1 7 3 2 向量函数微分定义和基本公式的m i z a r 实现1 8 3 2 1 向量函数微分的m i z a r 定义1 8 3 2 2 向量函数微分公式的m i z a r 证明1 9 4 向量函数偏微分的m i z a r 证明3 2 4 1 实现向量函数偏微分的指导思想3 2 4 2 向量函数偏微分的m i z a r 实现和基本公式的计算机证明3 2 4 2 1 环境部的设置和变量的声明3 2 4 2 2 向量函数偏微分在m i z a r 系统中的定义3 3 i i i 向量函数、微分及偏微分基本公式的计算机证明 4 2 3 向量函数偏微分基本公式的m i z a r 证明3 4 总结与展望4 l 参考文献4 2 致谢；4 5 攻读学位期间发表的学术论文目录4 6 声明4 7 青岛科技大学研究生学位论文 1 绪论 1 1m iz a r 系统的发展历史1 1 1 9 5 0 年，波兰著名数学家、逻辑学家a t a r s k i 在初等代数和几何的判定法 中推广了关于代数方程实数根数目的s t u r m 法则，从而证明了“初等几何和代数 范围的命题都可以用形式化方法判定，使数学形式化获得突破性进展，并为几 何定理的形式化证明开拓了一条利用代数方法的途径。2 1 二十世纪七十年代初，正在撰写拓扑学博士论文的a n d r z e jt r y b u l e c 教授萌生 了借助计算机撰写自己的数学论文的想法，并得到了俄罗斯全俄科学技术信息研 究所( v i n i t i ) 同行的支持。1 9 7 4 年秋，a n d r z e jt r y b u l e c 、k r z y s z t o fl e b k o w s k i 和r o m a nm a t u s z e w s k i 根据a t a r s k i 的形式化思想，合作设计完成了首个关于命题 逻辑的m i z a r 版本，并成功运行。1 9 7 5 年1 1 月，a n d r z e jt r y b u l e c 教授根据j a k o w s k i 自然演绎法完成了关于m j z a r 的初级版本m i z a r p c ( p r o p o s i t i o n a lc a l c u l u s ) ，之后 与r o m a nm a t u s z e w s k i 分别在华沙大学和华沙理工大学使用m i z a r - p c 教授命题逻 辑课程。 1 9 7 7 年，a n d r z e jt r y b u l e c 教授在m i z a r i 吾言中添加了量词，使系统升级到 m i z a r q c 1 2 0 4 ( q u a n t i f i e rc a l c u l u s ) 。同年，在a n d r z e jj a n k o w s k i 、r o m a n m a t u s z e w s k i 和p i o t rr u d n i c k i 的帮助下，8 月底a n d r z e jt r y b u l e c 教授用p a s c a l 语言编 译完成了新版本m i z a r - o c 6 0 0 0 。至u 1 9 7 8 年，m i z a r 系统中已经实现了包括集合论、 点阵理论和几何基础中许多定理的形式化证明，并且充实了语义、改进了句 法，新定义了p r e d i c a t e ( 谓词) 、s c h e m e ( 结构) 、s p e c i f i c a t i o n ( t y p e ) d e c l a r a t i o n ( 预 声明) 、a b s o l u t ee q u a l i t y ( 绝对相等) 、r e l a t i o n ( 关系) 和f u n c t i o n ( 函数) 等概念。 1 9 7 8 年，系统进一步优化升级为m i z a r m s ( m u l t is o r t e d ) ，开发出了两个大 的文本文件e 1 z b i e t ar a m m 和e d m u n dw o r o n o w i c z 用w i n k o w s 虹推理法证明了 阶乘算法程序的正确性 1 3 1 ；j e r z yz a b i l s k i 和r o m a nm a t u s z e w s k i 完成了几何原 理一书2 7 - 3 8 页的所有定理的形式化证明。1 9 7 9 年，m i z a r 系统中增加了函数符 号，改进了函数和关系的定义，系统升级至m i z a r - f c 。 1 9 8 1 年，第一个可解压缩的系统m i z a r - 2 设计完成。随着它不断的完善，m i z a r - 2 可以在m m 和u n i x 等多种不同的机器安装和运行，并且在论文中首次设置了 e n v i r o n ( 环境部) ，证明了语法的正确性，使用m i z a r 进行形式化证明更加便利。 1 9 8 2 年，a n d r z e j 教授在m i z a r - 2 设计了中间文件，使系统升级至m i z a r - 3 ， 向量函数、微分及偏微分基本公式的计算机证明 这是第一个多步骤处理的m i z a r 系统。在该系统中，根据各种正确性条件和不同定 义的需要添加了e x i s t e n c e ( 存在性) 、u n i q u e n e s s ( 唯一性) 、c o h e r e n c e ( 一致性) 、 c o n s i s t e n c y ( 相容性) 、c o r r e c t n e s s ( 正确性) 等关键词并沿用至今。 同年，为了扩充系统数据容量、使语言描述更加准确易懂，r o m a n m a t u s z e w s k i 、p i o t rr u d n i c k i 和a n d r z e j 教授一同在m i z a r 2 系统中定义了一个子语 言m i z a r m s e ( m u l t i s o r t e dp r e d i c a t ec a l c u l u sw i t he q u a l i t y ) ，解决了上述问题， 系统随之升级至l j m i z a r - m s e 版本。这个版本获得了巨大成功，被欧洲和北美洲的 许多大学用来讲授逻辑学和部分数学内容。1 9 8 3 年8 月在波兰华沙召开的第十九 届国际数学家大会上，a n d r z e j 教授出席了大会并做了发言：介绍了m i z a r 系统并 演示了如何用m i z a r - m s e 版本证明命题“i f t h eu n i o no f t w oe q u i v a l e n c er e l a t i o n si s f u l lt h e no n eo ft h er e l a t i o n si sf u l l ”。 1 9 8 3 年，a n d r z e j 教授在m _ i z a r 3 系统的基础上整合t m i z a r m s e 系统，实现了 新版本m i z a r - h p f ( h i d d e np a r a m e t e r sa n df u n c t i o n s ) 。 1 9 8 6 年，a n d r z e j 教授在同事的帮助下对m i z a r - 2 系统进行重新设计并吸收了先 前所有版本的优点实现j m i z a r - 4 ，这是一个重大的突破，现在所用的版本都是在 m i z a r - 4 系统基础上升级而来的。同年底，m i z a r - 4 成功在个人电脑上安装并运行。 经过两年多的发展，这个版本被a n d r z e j 教授称之为p c m i z a r ( p e r s o n a lc o m p u t e r ) 。 次年1 月1 日，m i z a r 数学数据库( m i z a rm a t h e m a t i c a ll i b r a 哕m m l ) 启用。 1 月6 日，收录了第一篇标准的i v l i z a r 论文_ b d o 切以p r o p e r t i e so f s e t s 6 。在随后 的2 0 多年里，m i z a r 系统是伴随着m m l 0 - 充而升级的。4 月，a n d r z e j 教授在m i z a r 系统中融合了排版软件r e x ，使m i z a r 系统具有自动排版功能，增强了m i z a r 论文 的可读性。1 9 9 0 年，出版了基于m _ i z a r 语言的专业期刊f o r m a l i z e dm a t h e m a t i c s 。 1 9 9 5 1 9 9 7 年间，m i z a r 系统的发展得到了美国海军研究总署的科研基金支持。2 0 0 1 年，g r z e g o r zb a n c e r e k 教授在文档检索工具g r e p 的基础上增加了用于查询语义的 功能，进而将g r e p 发展成为m m lq u e r y 。2 0 0 2 年，m i z a r 数学百科全书 e m m ( e n c y c l o p e d i ao fm a t h e m a t i c s i nm i z a r ) 开始建设并不断完善。 目前，已设计完成了在各种操作系统上安装并运行的不同m i z a r 版本，收录了 近一千一百篇论文，包含了近一万个定义、五万条定理，内容几乎含盖了数学领 域的所有学科，并拥有当今世界上最大的数据库m m l 。m j z a r 系统已成为集逻辑 证明、推理演绎、校验排版、复杂计算、科研教学功能于一体的形式化系统，同 时在自动化控制、声音和图像识别等研究领域有着广泛的应用，【7 】世界上许多 大学的学者参与t ! u m i z a r 的研究中。 2 青岛科技大学研究生学位论文 1 2miz a r 论文简介 m i z a r 语言是按照数学符号的一般表达式、英文表述与a s c i i 码相结合的原则 来定义和编写的，并且m i z a r 语言只能用计算机键盘上的数字、字母和其它符号来 表述。 1 2 1 论文结构 每一篇m t z a r 论文都是一个文本文件，可以通过新建伍t 文件并将扩展名改 为m i z 而得到。论文结构包括两部分：e n v i r o n ( 环境部) 和m a i ns e c t i o l l ( 正文部分) 。 其一般结构如下所示： e n v i r o n e n v i r o ns e c t i o n ( 环境部) ； b e g i n l a i ns e c t i o n1 ( 正文1 ) ； b e g i n l a i 。ns e c t i o n2 ( 正文2 ) ； b e g i n l a i ns e c t i o nn 正文n ) ： 1 2 2 环境部 e n v i r o n ( 环境部) ，既是每篇m i z a t 论文具体的运行环境，又是该篇论文的参 考文献。具体分为五种类型： 1 v o c a b u l a r i e s ( 词汇) ，是论文引用的词汇列表，同时也表明了算符词汇的 运算优先级； 2 s i g n a t u r e s ( 符号) ，包括n o t a t i o n s ，c o n s t r u c t o r s ，r e g i s t r a t i o n s ，r e q u i r e m e n t s 四个部分，m _ i z a r 论文中的所有符号都涵盖在s i g n a t u r e s 内； 3 d e f i n i t i o n s ( 定义) ，告知了论文中定义的出处： 4 t h e o r e m s ( 定理) ，是论文引用的定理列表； 5 s c h e m e s ( 模式) ，表明了论文的所引用的结构模式( 并不是每一篇m j z a r 论文需要引用结构模式) 。 环境部的一般结构如下： e n u i r o n v o c a b u l a r i e sa 1 。a 2 ，。a n ； n o t a t i o n sb 1 ，b 2 。b n ； c o n s t r u c t o r sc l ，c 2 ，c n ； r e g i s t r a t i o n sd 1 ，d 2 。，d n ； r e q u i r e m e n t se 1 ，e 2 ，e n ； d e f i n i t i o n sf 1 。f 2 。f n ； t h e o r e m sg 1 ，g 2 ，b n ： s c h e m e sh 1 。h 2 。h n ： 3 向量函数、微分及偏微分基本公式的计算机证明 ( a l ，a 2 ，a n ，x 1 ，h 2 ，h n 表示被引用f f t j h i z a r 论文在系统中的名称， 且这种名称不能超过八个字符) 1 2 3 正文部分 论文的正文部分首先要r e $ e l w c ( 假设变量) ，之后一般包括作者所作的 s t a t e m e n t ( 数学术语) 、d e f i n i t i o n ( 定义) 以及与定义相关的性质( a s s e r t i o n ， t h e o r e m ，e x a m p l e l ( 见图2 2 ) 。通过概念的m i z a r 定义，性质、定理、公式、推论 及特例等的形式化证明，从而实现理论体系的m i z a r 转化，使得数学理论在m i z a r 系统中继续发展。 鳓a t e r a e n t 国掰n 掰f 8 r 2 - 1m i z a r f f - 文部分的内容组成 f i g 2 - 1 t h ec o n t e n to fm i z a r 1 2 4 语言的综合使用 在撰写m _ i z a r 论文过程中，我们首先使用自然语言对所要证明的数学问题进 行分析，提出在m _ i z a r 程序中所应完成的功能( 即论文环境部的完善) ，从而使用 m i z a r 语言设计完成所证问题的计算机程序。从对问题的分析、环境部的设计到 程序的设计完成，是一个模型抽象、表示与组织的过程，这种形式化的表示正是 运用数学语言、算法来实现的。图2 一l 给出了一个语言使用示例t 4 青岛科技大学研究生学位论文 图2 - 2 语言使用示例 f i g 2 - 2 t h ee x a m p l eo fl a n g u a g eu s a g e 1 3 课题研究的主要内容 向量分析足数学中的重要分支，是关于两个维度及以上的多元实分析。它有 一整套的方程式及难题处理技巧，对物理学和工程学的发展有极大地帮助。虽然 m i z a r 数学库中知识储备庞大，但是关于向量函数的内容还没有涉及。 本课题的研究是建立在对数学定理的形式化证明和对m i z a r 系统及其语义、语 法深刻理解的基础上，在系统中利用m j z a r 语言和庞大的数学数据库m m l ，对向 量函数、微分及偏微分的理论和算法进行研究。为向量函数积分及微分几何的内 容在m i z a r 系统下的实现奠定理论和实践基础。 本文主要从以下几个方面在m i z a r 系统中进行研究： 1 基于m i z a r 中对于度量空间和欧氏空间定义的理解，给出了向量函数的 m i z a r 表示，在此基础上进而讨论了向量函数的有关性质。 2 在m i z a r 系统下，借助实函数可微性的定义，给出向量函数微分定义的 m j z a r 形式，并证明了向量函数微分的基本公式。 3 利用m i z a r 系统中规范线性空间的偏微分算子，实现了向量函数偏微分的 定义，并完成了向量函数偏微分的基本公式的形式化表示。 本文围绕向量函数的内容展开，主要讨论了向量函数及其微分、偏微分的性 质和相关公式。创新之处是在m j z a r 系统中首次定义了向量函数、微分及偏微分的 概念，建立了一个关于向量函数微分学、偏微分学较为完整的理论体系，并实现 了形式化表示，系统地完成了数学理论的m i z a r 转化。 1 4 课题研究的目的和意义 用计算机对数学问题进行形式化证明是数学科学与计算机技术结合产生的 新学科，随着计算机技术的高速发展，该研究领域是数学问题的复杂计算与繁琐 证明的必然要求。 m i z a r 系统具有撰写和检验数学论文的双重功能。目前，数学中许多领域的绝 大多数定理都可以利用m i z a r 系统进行验证，诸多复杂的数学定理已实现了形式化 证明，一些难以证实的猜想得到了初步证明，并且发现了一批新定理。m i z a r 系统 的不断自我完善与发展，提升了m i z a r 系统的处理能力，加速了与其它形式化系统 的交叉研究和相互转化。此外，m j z a r 系统具有智能性的“人机对话功能，可通 5 向量函数、微分及偏微分基本公式的计算机证明 过系统检测出论证的不当之处，提高了使用m i z a r 系统的科学性和安全性。 m i z a r 系统还为数学形式化和其他领域的形式化研究提供可行的新方法、新思 路、新工具。日本国立信州大学的中村八束教授，利用m j z a r 系统证明了j o r d a n 曲 线定理，并将m j z a r 系统广泛应用于数字信号传输、音像识别、自动化控制和微型 机器人等多方面的研究。 本课题利用m i z a r 系统把数学问题的证明思想与证明过程通过m i z a r 语言编译 在计算机上实现出来，其本身是一个机器智能化的过程，具有一定的难度与理论 意义。 6 青岛科技大学研究生学位论文 2 向量函数的m i z a r 实现 微分几何研究微分流行的性质，是现代数学的主流；同时是广义相对论的基 础，与拓扑学、代数几何及理论物理有着密切的关系；向量分析的知识广泛地应 用于微分几何中，对微分几何的研究提供极大地便利。而向量分析始于十九世纪 中叶，近年来已成为数学工作者、物理工作者和其他学科工作者必需的数学的基 础内容，并在自然科学与工程技术中有着广泛的实际应用。 目前，在m i z a r 数据库中缺少向量函数的m i z a r 实现，关于向量函数的具体的 系统理论也没有论述。本章主要介绍如何将上述内容在m i z s x 系统中实现形式化的 证明。 2 1 预备知i 只 2 0 1 本节就向量函数的定义、性质做一些介绍。 定义2 1 1 设g 是空间中一区域，雄) 、y ( f ) 、z ( t ) 是定义在g 内的实值函数，则 r = r = ，k t ) ，坝嘞为g 上的一个三元向量函数，其中z o ) ，) ，o ) ，z ( t ) 称为厂o ) 的坐标函数。 命题2 。1 。1 - ( 1 ) 三元向量函数( f ) 按基向量的分解式为柏= 删q + m 乞+ 荆岛； ( 2 ) 若r = r ( x 1 ，m ，五) ，s = 毗，y 2 ，乞) ，则 r s = “ 土恐 m 土虼 ，气 乞( 功； ( 3 ) 【2 5 】向量函数也满足矩阵的特殊运算“点乘法( “点 乘法实际 上是对相同维数的矩阵的对应元素进行相应的乘法运算) ：若r = 如，m ，互) ， s = s 如，兄，z 9 ，则厂木s = “ 而( f ) ，咒 毙 气 乞嘞； ( 4 ) 若r = r ( x a ，m ，互) ，s = 眠，兑，乞) ，则数量积( 点积) 7 向量函数、微分及偏微分基本公式的计算机证明 ，s = x 1 恐 + m 娩 + 五 乞( f ) ； ( 5 ) 若；= 。r ( x a ，y a ，互) ，则模阼原再丽：万丽； ( 6 )若r = r ( x a ，m ，气) ， s = s ( x 2 ，y 2 ，乞) ， 则向量积( 叉积) r x s = 瓴o ) z 2 一气 兄 ，气 x 2 一五 z 2 五 y 2 一m 。恐； ( 7 ) 若r = r ( x a ，y a ，互) ，s = s ( x 2 ，y 2 ，z o , u = u ( x 3 ，乃，z 3 ) ，则三重纯量积( 混合积) 满f f = r o 的= s x r ) = u ( r x s ) = r s x u 。 2 2 向量函数定义的m i z a r 实现及其性质的证明 利用m i z a r 系统进行数学问题的形式化证明具有刻板化和规格化的特点，为达 青岛科技人学研究生学位论文 添加到环境部中，而在论文完稿优化过程中如果有多余的引用系统通过检测会提 示我们删除，所以说刚开始建立的环境部并不是完善的。由于本文有新定义的函 子，因而在e n v i r o n 的v o c a b u l a r i e s 中需要添加本文的m m l 名e u c l i d8 ，便于 系统识别、检测。 随后，输入b e g i n ，表明论文正文的开始；接着声明论文中使用的变量的数 据类型： r e s e r v ea ，b ，c - d ，a l - a 2 ，a 3 ，b 1 ，b 2 ，b 3 ，r ，r 1 - r 2 ，r 3 ，x - ，。z ， x l 。x 2 ，x 8 ，1 ，9 2 ，y 3f o re l e m e n to fr e a l ； r e s e r v ef 。g ，f 1 。f 2 ，f 8 ，g l ，9 2 。9 3 ，h 1 ，h 2 ，h 3f o rf i n s e q u e n c eo fr e a l ； r e s e r v er - r 1 ，r 2 。r 8f o re l e m e n to f3 - t u p l e so nr e a l ： r e s e r v ep ，q ，p l ，p 2 ，p 3 。q l ，q 2 ，q 3 lf o re l e m e n to f r e a l8 ； r e s e r v ef 1 - f 2 ，f 3 。9 1 ，9 2 ，9 3 ，h l ，h 2 ，h 8f o rp a r t f u n co fr e a l ，r e a l ； r e s e r v et 。t 8 t l ，t 2f o rr e a l ； 2 2 2 向量函数定义的miz a r 实现 定义2 1 1 给出了向量函数的数学表达式。在m 1 z a r 中，应该以f u n c t o r s ( 函子) 形式定义，f u n c t o r s 定义可以看作是在m 娩a r 中定义一个新的概念，其标志性的词 是“f u n c 和“m e a n s ( + 句子) 或e q u a l s ( + 词语) ；并且要证明其e x i s t e n c e ( 存 在性) 和u n i q u e n e s s ( 唯一性) ；由于“向量函数 这个词的英文为“v e c t o rf u n c t i o n ， 因此按照定义f u n c t o r s 的一般原则定义其m i z a r 形式为v f u n c ：这是个三元向量函 数，因此它的变量有三个。假设变量为n 、亿、f 3 ，且属性类型为r 寸尺的p a r t f u n c ， 这样三元向量函数的完整m 瞌g a r 形式为v f u n c ( f l ，f 2 ，f 3 ) ，属性类型为r 一足3 的 f u n c t i o n ，在数值上等于l 【f 1 t ，亿t ，f 3 t 】l 。这表明此定义是在三维欧氏空间中向量 定义的基础上派生出来的，显示了m 泣a r 定义具有后延续性。新定义的f t m c t o r s 用 陈述性语句表述并且后面接的是一个句子，因此应该用m e a l l s 连接。然后，在m j z a r 系统中新建子文件夹，命名为d i c t ( 如果论文中有新定义，那么这个文件夹是必 须的，而且必须命名为d i c t ，这样系统才能识别) ，在此文件夹中新建名为 e u c l i d 文件，并将扩展名改为，在其中录入新定义的函子，并在 其前加o _ 表8 示的函子。向量函数形式化v 的o 表c 达和证明的结构如下： v f u n c d e f i n i t i o n l e tf l ，f 2 ，f 3b ep a r t f u n co fr e g l 。r e a l ： 弛墼u f u n c ( f l ，f 2 ，f 3 一 f u n c t i o no fr e a l ，r e a l3 m e a b s f o rth o l d si t t l lf 1 t ，f 2 t 。f 3 t 】i ； e x i s t e n c e _ p r o o f e n d ； ： ，7 1 1 9 向量函数、微分及偏微分基本公式的计算机证明 ： 7 8 ：s o m e t h i n gr e m a i n st o b ep r o u e d 经 j z a r 系统检测，在命令提示符中显示有两处错误，用文本文档打开论文， 出现两个标记为“7 0 ”的错误( 在论文最后系统提示标号“7 0 ”表明缺少证明过 程) 。完成“e x i s t e n c e 和“u n i q u e n e s s 的证明，“7 0 ”的错误就可去除。 首先证明e x i s t e n c e ，即证明确实存在r 哼r 3i 勺f u n c t i o n ：v f u n c ( f l ，亿，f 3 ) 满足定 义域为尺并且对露中的任一点，其函数值为i 【f 1 t , f 2 t , f 3 t 】i 。具体证明如下： e x i s t e n c e p r o o f d e f p r e d ( 预定义谓词) p s e t ，s e t m e a n ss 2 = l 【f 1 s 1 。f 2 s 1 。f 3 s 1 】l ；( 1 ) n 1 ：f o rxb e i n ge l e m e n to fr e a le x9b e i n ge l e m e n t o fr e a l8s te x 9 】； c o n s i d e rfb e i n qf u n c t i o no fr e a l 。r e a l3s u c h t h a tl a 2 ：f o rtb ee l e m e n to fr e a lh o l d sp 【t ，f t 1 ( 2 ) 篓婴绰构蝗鑫瓢魏2 竺竺! ：兰! 三! 空! ! 璺! ! ； j 丽f ，i i ：总结证明 j t h u st h e s i sb ya 2 ； ( 1 ) 是定义形式化证明过程中的预定义谓词，其标志为“d e f p r e d m e a n s ”。( 2 ) 是借助了结构模式f u n c t2 ：s c h3 说明函子的存在性：a 2 要成 立需要具备两个条件：一个是f u n c t2 ：s c h3 ，另一个是a 1 。 在v l _ i z a r 中，依据引导词有两个：b y 是一般依据引导词，引导直接的结论依 据，此依据可以是已经收录在数据库中的定义或定理，也可是正在撰写的论文中 前面已证明成立的命题；f r o m 是结构依据引导词，它和b v 的功能基本一致，所 不同的是f r o m 引导的结论依据必须引自结构模式s c h e m e 。在上述证明中，虽然 用到了一般依据a 1 ，但以结构依据f u n c t2 ：s c h3 为主，引导词要用“f r o m ， 这两个依据的连接不同于一般依据用“，”隔开，而要将f u n c t2 ：s c h3 前置， a 1 后置并置于“( ) ”内。 结构模式f u n c t2 ：s c h3 在m i z a r 中的具体表述为2 6 1 ： s c h e m e ：f u h c t _ 2 ：s c h3 f u n c e x d c ，d ( ) 一 n o ne m p t ys e t ，p s e t ，s e t ：e xfb e i n gf u n c t i o no fc ，d ( ) s tf o rxb e i n ge l e m e n to fc ) h o l d sr x f x 】 p r o u i d e d f o rxb e i n ge l e m e n to fc ) e x ，b e i n ge l e m e n to fd ( ) s tp x ，】； 引用这个结构模式，证明了定义的存在性，用“t a l 【ef ”语句作总结证明。 1 0 _ 墨一e 一 矗一 引一蛙 u f 7 堡o ， i o d 一、曩 n r n ：n u p e e 青岛科技大学研究生学位论文 然后证明u i l i q u e n e s s 。我们假定f ，g 是属性类型为r _ r 3 的f u n c t i o n ，且满 足题设条件，只需证明f = g 即可。 u n i q u e n e s s p r o o f l e tf ，eb ef u n c t i o no fr e f l l ，r e a l3 ： a s s u m e ( 假设词引导假设条件) t h a t n j ：f o rth o l d sf t = i 【f 1 t ，f 2 t ，f 3 t r 5 ：f o rth o l d sb t ；l 【f 1 t ，f 2 t ，f 3 t n o w ( 弓i 导扩散性命题) l e ttb ee l e m e n to fr e a l ； i f t2 i 【f 1 t ，f 2 t 。f 3 t 】ih 9n | i ；7 h e n c e ( 结论引导词) f t = g tb pr 5 ；l e n d ；j h e n c et h e s i sb p f u h c t 一2 ：1 1 3 ； h e n c et h e s i sb y f u h c t 一2 ：1 1 3 ； ：唯一陛得证 e n d ； ( 3 ) 说明了假设f ，g 满足题设条件：a s s u n i c ( 假设词) 用于引入命题的条件， 这里由于假设条件都是句子，用“a n d 连接，因而在a s s u m c 之后应加t h a t ，后 面必须有标号，且t h a t 之后不可以有t h e n 。( 4 ) 是一种扩散性命题证明方法，这种 证明方法以“n o w 为开始词，由此引出假设l e t t b e e l e m e n t o f r e a l ，通过推导 以“h e n c e 得到f t = g t 的结论，从而完成子命题f = g 的证明