（应用数学专业论文）四元数混合运算及特殊函数的微分公式和洛尔定理应用的mizar实现.pdf

青岛科技大学研究生学位论文 四元数混合运算及特殊函数的微分公式 和洛尔定理应用的m i z a r 实现 摘要 数学问题的机器证明是利用计算机证明和求解数学问题。m i z a r 语言系统是 上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的计算机语言系统。 如今该系统已拥有自身的数据库m m l ，收录了几乎涵盖数学各个分支的1 0 0 0 多 篇数学论文。同时，m i z a r 语言系统在自动化控制、声音和图像识别等研究领域 也有着广泛的应用。 本文首先介绍了定理机器证明和m i z a r 语言系统的发展历史，其次简单描述 了m i z a r 系统下定理机器证明和校验数学命题的方法，在此基础上对四元数的混 合运算，特殊复合函数的微分以及罗尔定理的应用等方面进行了m i z a r 实现。 本文主要工作： 1 在m i z a r 系统中定义了有关四元数的几个概念，完成了四元数的混合运算 性质的m i z a r 实现，对于四元数模的一些相关命题也进行了一定的m i z a r 论证。 2 基于m i z a r 数据库中已有的三角函数、幂函数、对数函数及可微性定理， 成功地对一些特殊复合函数的微分进行了m i z a r 实现。 3 将m i z a r 系统中己实现的罗尔定理与相关数学知识相结合，在m i z a r 系统 中实现了罗尔定理和柯西中值定理的一些应用和推广。 以上结果均已通过m i z a r 语言系统的验证，部分内容已被收录在m i z a r 数据库 m m l 中。 关键词：机器证明m _ i z a r 四元数微分罗尔定理 青岛科技大学研究生学位论文 m i x e do p e r a t i o no fq u a t e r n i o n ， s p e c i a lf u n c n o nd i f f e r e n t i a t i o na n d a p p u c a n o no fr o l l e st 哑o r e mi nm i z a r a b s t r a c t a u t o m a t e dt h e o r e mp r o v i n gf o rm a t h e m a t i c sm e a n st od e m o n s t r a t ea n dc a l c u l a t e t h em a t h e m a t i c a lp r o b l e m sb yc o m p u t e r m i z a rs y s t e mi si n i t i a t e da sac o m p u t e r s y s t e ml a n g u a g eo fl o g i c a lp r o o f , v a l i d a t i o n ，a n dt y p e s e ti nt h e1 9 8 0 s n o w a d a y s ，t h i s s y s t e mh a so w n e ni t sd a t e b a s e ( m m l ) a n de m b o d y e dm o r et h a n1 0 0 0m a t h e m a t i c s p a p e r sw h i c hi n v o l v e sa l m o s te a c hb r a n c ho fm a t h e m a t i c sf i e l d m e a n w h i l e ，m i z a ri s w i d e l yu s e di nr e s e a r c ha r e a ss 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 dp a t t e r n r e c o g n i t i o n t h i sp a p e rf i r s t l yr e v i e w st h eh i s t o r yo fa u t o m a t e dt h e o r e mp r o v i n ga n d m i z a r , t h e ng i v e sad e s c r i p t i o no fm e t h o d so fm e c h a n i c a lt h e o r e mp r o v i n ga n d v e r i f i c a t i o nt om a t h e m a t i c a lp r o p o s i t i o nu n d e rm i z a rs y s t e m b a s e do nt h a tb a s i s ，t h e p a p e rh a sd o n es o m em i z a r r e s e a r c h e so nm i x e do p e r a t i o no f q u a t e r n i o n ，d i f f e r e n t i a t i - o no fs p e c i a lc o m p o s i t ef u n c t i o na n dt h ea p p l i c a t i o no fr o l l e st h e o r e m t h em a i nw o r ko ft h i sp a p e ri sa sf o l l o w s ： f i r s t l y , s e v e r a lc o n c e p t sa b o u tq u a t e m i o na l ed e f i n e di nm i z a rs y s t e m t h ep a p e r d i s c u s s e st h em i z a ri m p l e m e n t a t i o no fm i x e dm o d e a r i t h m e t i c a lf o rq u a t e r n i o na n da l s o d o e ss o m ei n t e r r e l a t e dm i z a rv e r f i c a t i o n so nm o d e lo fq u a t e m i o n s e c o n d l y ，b a s e do nt h et r i g o n o m e t r i cf u n c t i o n ，p o w e rf u n c t i o n ，l o g a r i t h m i cf u n c t i o na n dd i f f e r e n t i a b i l i t yt h e o r e m s ，a l lo fw h i c hh a v ea l r e a d yb e e ni m p l e m e n t e di nl v l i z a r s y s t e r r n ，t h ep a p e rh a ss u c c e s s f u l l yi m p l e m e n t e dt h ed i f f e r e n t i a t i o no fs o m es p e c i a l c o m p o s i t ef u n c t i o n sw i t l lm i z a rs y s t e n n t h i r d l y , t h ep a p e rc o m b i n e sm a t h e m a t i c a lk n o w l e d g ew i t ht h er o l l e st h e o r e m i m p l e m e n t e di nm i z a rs y s t e ma l r e a d y , i m p l e m e n t st h ee x e r ta n dp r o m o t i o no fr o l l e s t h e o r e ma n dc a u c h ym e a nv a l u et h e o r e mi nm i z a rs y s t e m 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 t h ep r e s e n tr e s u l t sh a v eb e e nv e r i f i e ds u c c e s s f u l l yb ym i z a rs y s t e m ，a n dp a r t i a l c o n t e n t sh a v eb e e na c c e p t t e db ym i z a rd a t a b a s em m l k e yw o r d s ：a u t o m a t e dt h e o r e m p r o v i n g m i z a r q u a t e r n i o n d i f f e r e n t i a t i o n r o l l e st h e o r e m 青岛科技大学研究生学位论文 声明 独创性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中 不包含其他人已经发表或撰写过的研究成果，也不包含本人已用于其他学位申请 的论文或成果。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了 明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人躲王擤嗍：c 年舌月胪 关于论文使用授权的说明 本学位论文作者完全了解青岛科技大学有关保留、使用学位论文的规定，有 权保留并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅和借 阅。本人授权学校可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人离校后发表或 使用学位论文或与该论文直接相关的学术论文或成果时，署名单位仍然为青岛科 技大学。( 保密的学位论文在解密后适用本授权书) 本学位论文属于： 保密口，在年解密后适用于本声明。 不保密口。 ( 请在以上方框内打“”) 本人签名： 导师签名： 6 1 年么月侈日 年易月侈日 缪秘一衅狲 青岛科技大学研究生学位论文 1 绪论 1 1定理机器证明的历史及研究现状 定理机器证明r p ：a u t o m a t e dt h e o r e mp r o v i n g ) 一般被称作自动推理，它以 计算机为辅助工具对数学问题的定理及结论进行推理，演算和验证，是- - f - j 数学与 计算机科学的交叉学科，也是人工智能领域的一个重要分支。定理机器证明又称 定理证明的机械化，作为数学问题机械化的主要研究内容之一，它要求在运算或 证明过程中，遵循一定的操作规则和程序并且所有的程序步骤都要依据特定的法 则刻板地进行，也就是说机器证明体系不存在跳跃性。【1 】 历史上，早在1 7 世纪德国著名的数理逻辑学家、哲学家和微积分的创始人 之一莱布尼兹就已提出了机器证明的构想，设想建立一种演算，创造一种通用的 语言，以实现推理证明问题的机械化。1 9 5 6 年由纽厄尔、赫伯特西蒙等人合作 编制的逻辑理论机数学定理证明程序l o g i ct h e o r i s t ( 简称l t ) 使机器证明迈 出了逻辑推理的第一步。1 9 7 6 年，美国的哈肯( h a k e n ) 和阿佩尔( a p p l e ) 在高速计 算机上用了1 2 0 0 个机时解决了这个困扰了数学家们1 0 0 多年的难题，这是机器 证明首次解决传统人脑支配的手工证明所没有解决的重要难题。虽然还不能认为 那一种真正意义的机器证明，但足以表明计算机作为定理证明的辅助工具这一领 域有着巨大的潜力空间。2 0 纪7 0 年代我国定理机器证明的开拓者吴文俊院士提 出了利用机器证明发现几何定理的新方法，从初等几何着手，用计算机证明了一类 高难度的定理，同时发现了一些新定理，进一步探讨了微分几何的定理证明。f 1 1 现今，机器证明已涉及到机器人学、曲面造型、信息处理、计算机图形与 视觉、数控技术、智能c a d 、信息安全和数字图像的高速高保真传输等领域，为 一系列高科技问题的解决提供了有力的工具。此外，机器证明的应用也在分析拓 扑学、集合论以及递归函数等方面获得了成功。在我国机器证明及其应用的核心 内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。由于吴文 俊院士在7 0 年代的突出工作，我国在此方向上处于领先地位。 目前为止，已有1 5 种机器语言系统受到北美数学知识管理组织 ( n a ：m a t h e m a t i c a lk n o w l e d g em a n a g e m e n t ( m 讧) ) 及大多数专家的认可，如 a u t o m a t h 系统2 1 、m i z a r 系统3 ，4 1 、n u p r l 系统f 5 1 和t h e o r e m a 系统6 1 ，近来， 越来越受人们关注的还有a c l 2 7 i 和p v s 8 1 ，而可用来进行定理证明的机器语言 系统已将近3 0 0 种9 1 ，m 1 z a r 语言系统正是其一，且m i a z r 系统已具备大量的 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 m i z a r 系统数学数据知识库，这为m i a z r 语言的初学者提供了丰富的研究样板和 参考，也为m i a z r 语言系统的壮大发展注入了强心剂。 1 2m i z a r 系统的历史和研究现状 m i z a r 系统是在定理机器证明的发展过程中产生的集自然演绎、逻辑证明、复 杂计算、验证排版、科研教学于一身的计算机语言系统。m i z a r 系统有自己特定 的语法结构，证明模式，以及程序优化和结果验证体系。m i z a r 语言在数学问题 的计算机证明中得到了充分的利用和发展，拥有目前世界上最大的数学数据知识 库m m l ( 期刊f o r m a l i z e dm a t h e m a t i c s 的o n 1 i n e 版本) ，并不定期更新修正， m i z a r 爱好者可在i n t e m e t 上随时查阅最新版本。1 0 1 m i z a r 系统的形成始源于a n d r z e jt r y b u l e c 教授的一个想法：“是否能够借助于 计算机来撰写自己的数学论文? 在1 9 7 3 年1 1 月1 4 同华沙大学图书馆学和科 学信息学院的一次研讨会上，t r y b u l e c 教授第一次完整地提出了一种可实现的用 来撰写数学论文的计算机语言，并对这种语言在其功能上的一些必需的特点作了 说n e 1 1 ： 1 具有可存储性和可编译性，即撰写的文章可存储于计算机中，并可将其 全部或部分内容自动翻译成自然语言； 2 格式整齐匀称，内容简洁易懂； 3 具有支撑整个数学领域自动化信息系统的基本要素； 4 具有简便查验错误、查证参考文献、删减重复定理的功能； 5 可实现自动排版功能。 在m i z a r 语言系统中通过验证并得以运行的第一组数学定理是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 三位教授共同设计 完成的，从此m i z a r 语言系统有了雏形，虽然当时的版本运行速度和程序优化上 跟现在无法相提并论，但却不失正确的语言结构和语义。 1 9 7 5 年，m i z a r 语言系统得到波兰科学协会的支持，并开始被研究。在同年 1 1 月，a n d r z e j 教授提交了m i z a r 语言系统的初级版本m i z a r - p c ( p c 表示命 题演算) ，并且预见性的提出了数学数据库的问题，即1 9 8 9 年才设计成功的m i z a r m a t h e m a t i c a ll i b r a r y ( 简称m m l ) 。值得一提的是，1 9 7 5 年6 月，t r y b u l e c 教授 第一次以文字的形式展示他创建的m i z a r 机器证明语言，发表了一篇名为 “l o g i c i n f o r m a t i o nl a n g u a g em i z a r ”。同年1 1 月发表了一篇关于m i z a r - p c 的报道， 报道主要介绍了如何借助m i z a r 语言用j a g k o w s k i 自然演绎推理的方法撰写逻辑 谓词验算的证明过程。此时的m i z a r 系统已经可以用( 蛐e n d ) 、e n d ) 、 2 青岛科技人学研究生学位论文 ( 虹) 、0 e _ t ) 、( t h u s o r h e n c e ) 这样的语义词来编写定理。 1 9 8 9 年m m l 开始投入使用，并且随着m m l 的不断扩充，m i z a r 语言系统 也在不断的更新升级。1 9 9 0 年，( ( 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 期刊f o r m a l i z e dm a t h e m a t i c s 得到了美国o f f i c eo fn a v a l r e s e a r c h 的资金支持 1 2 1 。2 0 0 2 年，m i z a r 数学百科全书e m m ( e n c y c l o p e d i ao f m a t h e m a t i c si nm i z a r ) 完成【1 3 】。 目前m i z a r 数据库收录了来自波兰、日本、中国、加拿大等多个国家的教授学 者和研究生撰写的数学论文。m i z a r 语言系统发展到今天已更新至7 1 1 版本，m m l 为4 7 2 版本，内含1 0 0 0 多篇文章，2 力多个数学定义，将近4 0 万条定理。 1 3 课题研究的主要内容 自1 9 8 9 年m i z a r 语言系统完全建立以来，数据库m m l 不断得到充实，已形 成著名的数学知识处理的形式化系统领域，其中涉及的数学知识如数学分析学、 代数学、几何学、数论、图论、范畴理论等几乎涵盖了数学的每一个分支。然而 有关四元数的混合运算，特殊复合函数的微分公式和罗尔定理的应用在m i z a r 数 据库中还很少见，本文的主要研究内容： 1 在m i z a r 系统中定义四元数的符号数，四元数的平方和立方，四元数的矩 和迹，完成了四元数混合运算的m i z a r 实现，同时也对四元数的一些性质和有关 四元数模的一些命题进行了m i z a r 论证。 2 基于m 1 z a r 数据库中已有的三角函数、幂函数、对数函数及可微性定理， 成功地对一些特殊复合函数的微分进行了m i z a r 实现。 3 将m i z a r 系统中已实现的罗尔定理和柯西中值定理，结合相关数学知识， 在m i z a r 系统中实现了罗尔定理和柯西中值定理的一些应用和推广。 本文主要以四元数的混合运算性质和有关微分的性质定理为出发点，以m _ i z a r 语言为工具实现了相关定理的m i z a r 论证，从而完成了相关数学理论的m i z a 语 言转化。 1 4 课题研究的目的和意义 本课题的研究是基于对数学定理自动推理系统m _ i z a r 及其语言的语义、语法的 深刻理解，借助m i z a r 语言系统庞大的数学数据库( m m l ) ，对有关四元数和微分 的内容做了m 1 z a r 论证，一定程度上促进了数学分析中的理论在i i z a r 中的机械 化实现，为进一步实现微分性质定理在v _ i z a r 系统中的的运用和推广做出了必要 3 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 的准备，同时也为以后四元数的微分，四元数矩阵以及八元数的m i z a r 实现提供 了可靠的m i z a r 依据和支持。 m z a r 语言系统是一个兼有撰写和检验数学文章功能的软件，它可以证明数学 学科中绝大多数问题。m i z a r 语言系统还为研究广泛领域的机械化数学和数学机 械化开辟了新道路，开拓了新思想，提供了新工具。 利用m i z a r 系统进行数学问题的自动推理证明，使计算机具备类似入脑的推理 能力，不单是促进了m i z a r 系统本身的完善也同样推动了数学学科的发展。现今 的m i z a r 语言系统已由单独的定理证明发展到多学科多方面的交叉应用，包括 m i z a r 语言的开发、m i z a r 数据库的扩充、m i z a r 自动推理能力的提高及m i z a r 翻 译形式的多样化处理四个方面的内容。 4 青岛科技人学研究生学位论文 2m i z a r 语言系统 2 1m i z a r 语言的安装和升级 m i z a r 语言程序可以直接移植到网络环境和单机上运行。同m i z a r 系统兼容 的平台有：f r e e b s d ( i 3 8 6 ) ，l i n u x ( i 3 8 6 ) ，d a r w i n m a c o s x ( p p c ) ，s o l a r i s ( i 3 8 6 ) ， l i n u x ( p p c ) ，a n dw i n 3 2 。 2 1 1m i z a r 语言的安装 步骤1 ： 在安装之前要设置下环境变量，右键单击我的电脑，选择“属性”，在“高级 选项卡里点击“环境变量”，在出现的系统变量栏双击“p a t h ，在变量值的最后 面添加“； ，最后键入：c ：k m i z a r ，至此环境变量设置完毕。 步骤2 ： 将下载的m i z a r 版本解压缩，双击其中的批处理文件“i n s t a l l b a t ”，出现d o s 界面：p r e s s e n t e rt oi n s t a l li n t oc s m i z a r ，回车后大约3 0 秒，m i z a r 系统即安装到 c ：m i z a r 。 步骤3 ： 如果要将m i z a r 系统安装到其他目录( 以d ：l m i z a r 为例) ，只需在步骤1 中 最后键入：d ：m i z a r ，在步骤2 出现d o s 界面后，输入i n s t a l ld ：w i i z a r ， 回 车即可。 2 1 2m i z a t 语言的升级 m i z a r 系统的升级包括两个方面：m j z a r 数据库m m l 文件的扩充( 即m i z a r 论文数量的增加) 和m i z a r 系统对已有数据的适时修正调整。所有m i z a r 论文的 完成需在最新版下运行以避免不必要的麻烦。为获得最新版本，可登陆下列网站 j a p a n ：f t p ：m a r k u n c s s h in s h u u a c j p p u b m iz a r p o l a n d ：f t p ：f t p m iz a r o r g 。 2 2m 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 形式的定义，下面对基本词汇进行简要介绍： 2 2 1m i z a r 语言的基本词汇 1 e n d ( 结构词l p r o o f 和e n d 在m i z a r 系统的证明中总是成对出现的，每出现一个p r o o f , 后面就 要有一个e n d 与之相对应，即p r o o f 和e n d 的个数必须相等。否贝j j m i z a r 证明将无法 正确地进行下去而且检测程序时也会出现错误提示。此外，p r o o f - e n d 作为一个完 整的句子，在其证明过程中出现的句子，般不可以被p r o o f - e n d 之外的证明引用。 2 b y ( 简单依据引导词) 和f r o m ( 结构依据引导词) 1 4 在m i z a r 语言系统中每个等式或结论的出现都要有依据，b v 就是引导这些依 据的词汇，这些依据可能是正在编写的文章中前面已证明成立的命题，也可能已 收录在m i z a r 数据库中论文的定义或定理。f r o m 与b v 的功能大致相似，区别在 于f r o m 引导的依据须是s c h e m e ( 一种结构模式) 。 3 c o n s i d e r 与t a k e ( “已存在取定”与“假设取定”) c o n s i d e r 与t a k e 在m i z a r 中均可译为“取定 ，但它们的词汇意义是不同的。 c o n s i d e r 是假设一个使命题成立的存在量，t a k e , i 题1 是取定一个使命题成立的存在 量，这个存在量是已经存在的并且满足命题成立的条件。 4 i m p l i e s ( 推导词) i m p l i e s 主要用于定理的表述，是条件与结论的连接词，而且条件和结论之间 要有间接的因果关系。 5 f o r h o l d s ( 全称命题) 1 4 ( 1 ) 含存在性定理表述 f o rmb e i n gs e ts to ( m ) h o l d se x1 1s tp ( n ，m ) ( 任给m ，满足q ( m ) ，能推出存在n ，使 得p ( n ，m ) 成立) 。 ( 2 ) 含条件定理表述 f o rmb e i n gs e ts tq i ：m ) h o l d sp ( m ) ( 任给m ，满足q ( m ) ，能推出p ( m ) ) ( 3 ) 一般定理表述 f o rmb e i n gs e th o l d sp ( m ) ( 任给m ，能推出p ( m ” 2 2 2m i z a r 语言的表达符号 m i z a r 系统的表达符号可以是纯粹的数学符号，可以是该符号的英文表述，也 可以用一般的a s c i i 字符来定义和编写的。下表列出了一些常见表达符号： 1 4 6 青岛科技大学研究生学位论文 普通数学命题中 vj = = 八m ) c =i f f 的逻辑符号 表2 - 1 普通数学命题和m i z a r 语言系统中的逻辑符号 2 3m i z a r 系统中的定义 2 3 1v o c 文件 每篇定义了新概念的m j z a r 论文都有一个属于它自身且与其同名的文档。该文 档以v o c 为后缀，记录了新概念的信息。由于定义类型不同，新概念的前面需用一 个大写字母标明其类型，具体对应关系如下表 1 5 ： s y m b o l s ( 代表字母)t h i n g st h a ta r ed e f i n e d ( 定义类型) r p r e d i c a t e ( 谓词) m m o d e ( 模式) o f u n c t o r ( 算子) l r i g h tf u n c t o rb r a c k e t ( 右括号) kl e f tf u n c t o rb r a c k e t ( 左括号) v a t t r i b u t e ( 属性) g s t r u c t u r e ( 结构) u s e l e c t o r ( 函子) 表2 - 2 定义类型的代表字母表 v o c 文件的创建规则及顺序为：先填写与定义类型对应的大写字母，其后紧接 新定义的词汇名，中间不可添加空格或其他字符。对于新定义的算子( f u n c t o r ) ， 在类型字母o 加新定义词汇名后，可添加空格和1 至u 2 5 5 之间的一个数字，其中数 字表示运算优先级，缺省表示6 4 。如m _ i z a r 文章i n t1 的词汇表d r r1 v o c 的创 建形式如下表： 7 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 表2 - 3i n1 v o c 的创建形式 2 3 2 定义分类 m i z a r 系统中的定义以定义合理、分类明确的特点。系统中的定义主要分为谓 词定义( p r e d i c a t e s ) 、模式定义( m o d e s ) 、算子定义( f u c t o r s ) 、属性定义( a t t r i b u t e s ) 、 c l u s t e r 定义、e q u a l s 定义和结构定义( s t r u c t u r e s ) ，其中定义的合理性体现在对于不 同分类的定义，需要从存在性和一致性两方面给出逻辑证明，如下 1 5 表“0 表示需要证明，无“0 ”表示无须证明。 e x i s t e n c e u n i q u e n e s s m o d e ( 模式) o f u n c t o r ( 算子) oo p r e d ( 谓词) c l u s t e r oo a t t r ( 属性) 表2 - 4 定义证明分类 2 3 3 重新定义 重新定义( r e d e f i n i t i o n ) ，是指对于m m l 中已存在的算子定义( f u c t o r s ) 、模 式定义( m o d e s ) 等在不改变原定义符号的前提下，改变其定义后的数据属性或定 义内容而重新定义。若要改变定义内容，即给出另一种定义形式，则需要证明前 8 青岛科技大学研究生学位论文 后两个定义具有兼容性c o m p a t i b i l i t y ；若要改变定义后的数据属性，需要证明重 新定义与原定义的一致性c o h e r e n c e 。 2 4m i z a r 系统中的证明方法 1 直接法 直接法是指直接从题的条件出发，经过合理的推导得出命题结论。如下面形 式的定理可用直接法完成证明。 t h e o r e m p x 】：p 【x 】是关于x 的一个命题 p r o o f ：推导过程 t h u s “x 】； e n d ； 2 分步法 分步法是将一个命题分为若干个独立的分命题，通过对各个分命题的证明， 最终完成对整个命题的证明。如证明命题p 【x 】& q 【y 】： t h e o r e m p x 】& q 【：p 【) q 是关于x 的一个命题 ：q 【是关于y 的一个命题 p r o o f t h u s p 【x 】； t h u sq 【； e n d ； 3 矛盾法 矛盾法又称反证法、 题条件矛盾的结论。 a i m p l i e sb p r o o f a s s t l m ea a s s u m en o tb ： 间接法，即假设命题结论的否命题成立，通过推导得出与命 矛盾法的使用标志是“c o n t r a d i c t i o n 。如： ：这个假设必须要有，否则检测时会出错 ：假设非b 成立 t h u sc o n t r a d i c t i o n ； ：证明矛盾，说明a 与非b 不能同时成立 9 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 2 5m i z a r 系统的文章结构 m i z a r 语言论文是以文本文件的形式出现的，一般的文本编辑软件均可用来 以编辑m i z a r 文章。m i z a r 论文分为环境部( e n v i r o n ) 和正文两部分，其中正文 又可以分为若干个独立小块，每个小块均以b e g i n 开始，换行后进行正文的书写。 大致结构如下： e n v i r o n 环境部设置 b e g i n 正文 b e g i n 正文 “环境部设置 相当于普通论文的参考文献，分类标出了该篇m i z a r 论文中 引用定理、函数和符号等的出处。环境部具体分成五类，分别是：v o c a b u l a r y , s i g n a t u r e ，t h e o r e m s ，d e f i n i t i o n s ，s c h e m e s 。其中，v o c a b u l a r y 部分包含了m iz a r 表 达式中所使用的词汇，同时也表明了算符词汇的运算预先级。s i g n a t u r e 部分( 包 括r e g i s t r a t i o n s 、c o n s t r u c t o r s 、n o t a t i o n 、r e q u i r e m e n t s 四部分) 通知m iz a r 处理器 这篇文章可以使用此处列出的文章里的符号。d e f i n i t i o n s 、t h e o r e m s 和s c h e m e s 用来标明使用m i z a r 基本指令检测论文时可以引用这些论文中的定理、定义和模 式等。 d e f i n i t i o n s ：a 1 ，a 2 ，a n ；定义引用 t h e o r e m s ： b 1 ，b 2 ，b n ；定理引用 s c h e m e s ：c 1 ，c 2 ，o n ；模式引用 其中础，b i ，c i ( i = 1 ，2 n ) 表示l i ，l j z a r 数据库中已收录的论文名字，它们分别 表示完成该篇m i z a r 论文需要引用论文加中的定义，b i 中的定理，c i 中的模式。 2 6m i z a r 系统的优化及检测命令 在m i z a r 论文的写作过程中需要不断地用m i z f 命令来检测论文，以保证程序 的格式、语法和证明逻辑的正确性，只有所写的程序完全通过m i z f 的检测论文才 可以继续进行下去。除了m i z f 之外，还有几个命令常用来优化l 、i i z a r 论文，使论 1 0 青岛科技人学研究生学位论文 文整体在证明繁琐程度和语法更加符合m i z a r 系统的要求。 是最常用的检测命令： 1 、r e l i t e r s检测文章中多余的运算步骤 2 、r e l p r e m 检测文章中多余的引用 3 、c h k l a b检测文章中多余的标号 4 、i r r v o c 检测环境部中多余的词汇 5 、r e l i n f e r检测文章中繁琐的表达 6 、i m h s 检测环境部中没有用到的定理 7 、i n a c c检测文章中多余的论证步骤 8 、t r i v d e m o 检测文章中繁琐的证明过程 值得注意的是这些命令的使用并没有固定的顺序可言， m i z f 检测以后才能用来检测。 1 1 以下是8 个最基本也 但都必须在论文通过 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 3 四元数混合运算的m i z a r 实现 在本文之前，m i z a r 数据库里已有两篇有关四元数的论文 1 6 ，1 7 ，主要给出 了四元数的几个基本定义和一般的运算法则，但关于四元数混合运算的m i z a r 实 现几乎没有涉及，有关四元数的一些性质和概念也有待补充。而有关四元数代数， 四元数矩阵和八元数的研究都需要对四元数及其运算性质有着深刻的理解，因此 有关四元数的混合运算及性质的m j z a r 实现对以后四元数代数，八元数，四元数 矩阵等在m i z a r 系统里的论证有着重要意义，对于m i z a r 系统的数据库也是很必 要的扩充。 3 1预备知识 本节简单介绍了四元数的定义，四元数的四则运算和四元数运算的基本法 则，旨在为本章正文的进行提供一定的理论支持。 3 1 1 几个定义 18 定义3 1 1 设z - - a - i - b i - i - c j - i - d k ，a , b ，c ，d r 其中i , j ，k 满足i2 = j2 = k 2 = 一1 , i j = - j i = k , j k = 一k j = i ，k i = 一k i - - j ，称z 为四元数，而a 称 为四元数的实部，记为r e ( z ) = a ，b i + c j + d k 称为四元数的虚部，记为i r a ( z ) = b i + c j4 - d k ，i , j ，k 称为四元数的虚部单位。 以下均设a , b ，c ，d r ， 定义3 1 2 a b i - c j _ d k 称为四元数z - - a4 - b i + c j + d k 的共轭，记为z 。 定义3 1 3口2 + 6 2 + c 2 + d 2 称为四元数z - - a - i - b i4 - 国+ d k 的模，记为i z i 。 定义3 1 4a 2 + 6 2 + c 2 + d 2 称为四元数z - a - i - b i + c j - i - d k 的矩，2 a 称为z 的 迹，分别记作为n ( z ) ，t ( z ) 。 定义3 1 5 设z 是四元数，若存在四元数p ，使得p z = l ，则称p 为四元数z 的倒数，记为z 一。 需要说明的是，定义3 1 3 和3 1 4 在本文之前m i z a r 系统中并没有被提及 过，本文在后面将给出它们m i z a r 形式的定义。 青岛科技人学研究生学位论文 3 1 2 四元数的加减乘除运算 设四元数毛aa l + b l i + c l j + 盔k ，z 2 一a 2 + 6 2 i + c 2 j + d 2 k ，则四元数的加法，减 法，乘法，除法分别规定如下 1 8 ： 气+ z 2 一( 口1 + 口2 ) + ( 6 1 + b 2 ) i + ( c 1 + c 2 ) j + ( d 1 + d 2 ) 七； z 1 一z 21 ( 口1 一a 2 ) + ( 6 l b 2 ) i + ( c l c 2 ) j + ( d 1 一d 2 ) 七； z l z 21 ( a l a 2 一b l b z c l c 2 一d l d 2 ) + ( 口l 吃+ b , a 2 + q d 2 一d l c 2 ) f + ( 口1 c 2 + a 2 c l + b 2 d 1 一d 2 b o j + ( 口1 d 2 + d l a 2 + 6 1 c 2 一c l b 2 ) 七； 乙z 2 = ( 口2 a l + 6 2 b l + c 2 c 1 + d 2 d 1 ) ( i z 21 2 ) + ( 以2 b l 一也口1 一c 2 d 1 + d 2 q ) l ( i z2i2 ) i + ( 口2 c 1 + b 2 d l c 2 a 1 一d 2 b 1 ) ( i z2 i2 ) j + 口2 d l - b ：l + c 2 l j l d 2 a 1 ) ( i z2 i2 ) k 。 3 1 3 四元数运算的基本法则 1 8 设毛，z ：，z 3 均是四元数，那么 z 1 z 2 z 31z l ( z 2 z 3 ) ； z 1 ( z 2 + z 3 ) 一乙z 2 + 乙z 3 ； ( z 1 + z 2 ) z 3 一z 1 z 3 + z 2 z 3 ； z 1 ( z 2 一z 3 ) 曩z 1 z 2 一z l z 3 ； c 毛一z 2 ) z 3 暑z 1 z 3 一z 2 z 3 。 3 2 四元数在m i z a r 系统中的表述 由于m i z a r 语言系统自身词汇表达的特殊性，很多数学定义在m i z a r 中的形式 和一般数学教材里的定义是不同的，四元数也不例外。如四元数z 的实部在m j z a r 中的形式是r e az ，三个虚部单位分别是 ， ， b ，一般的四元数z 在 v i z a r 中 可以表示成如下形式：1 6 1 z = r c a z + i m lz + ( h n 2 z ) 木 + ( t i n 3z ) 木 ； 也可以将z 表示成 * r e az ，i m lz ，i m 2z ，i m 3z 1 。其中i m lz 习惯上称为四元数z 四元数混合运算及特殊函数的微分公式和洛尔定理应用的m i z a r 实现 的第一个虚部，i m 2z ，i m 3z 顺称为第二个和第三个。m i z a r 中四元数z 的倒数表 示为z ”，四元数z 的共轭和模分别表示为z 木和1 z i ，而四元数中的0 和1 则分别表 示为0 q 和1 q 。有关四元数理论知识的m i z a r 形式可以参考m i z a r 数据库中 q u a t e m i m i z 1 6 和q u a t e m 2 m i z 1 7 。 3 3 环境部的设置 在m i z a r 论文的初始部分需要设置好大致环境部( e n v r i o n ) ，为j 下文中数学问 题的m i z a r 表述与证明可能用到的定义，词汇，定理等提供相关的m _ i z a l ；支持。 但环境部并不是一直不变动的，在论文的进行过程中，要根据论文需要对环境部 各部分进行相关的增减，下面给出论文完成时环境部的最终形式： e n v i r o n v o c a b u l a r i e s a r y t m ，r e l a t1 ，c o m p l e x l ，q u a t e r n i ，f o n c r _ 4 ， a r v t m j ，a r y