（应用数学专业论文）基于mizar的函数奇偶性及周期性的研究.pdf

川i i ii i ii ii ii rl lr l f liii 青岛科技人学研究生学位论文 y 17 4 0 2 6 3 基于m i z a 瓜的函数奇偶性及周期性的研究 摘要 数学问题机械化是指用计算机推理、证明、计算数学问题和定理。目前，世 界各国都在积极地进行数学问题机械化的研究，比较著名的数学定理证明系统有 m i z a r 、p v s 、c o q 等，而m i z a r 语言系统凭借其庞大的m m l 数据库和其优越的 功能，得以快速发展，深受世界各国的重视。m _ i z a r 语言系统已经发展成为集众 多功能于一体的数学知识处理系统，目前m m l 数据库已经收录1 0 9 0 多篇数学论 文，其内容几乎涵盖了数学的各个分支，尤其是在拓扑学及泛函分析学等学科的 定理证明中更突显出m i z a r 语言系统的优越性。 本文首先介绍了l v l 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 系统下实 现； 2 在m i z a r 系统下给出了周期函数及周期的定义； 3 基于m i z a r 系统论证了奇函数、偶函数及周期函数的性质以及某些复合函数 的奇偶性及周期性； 4 在m i z a r 系统下，证明了一些初等函数的奇偶性及周期性，例如：常函数、 符号函数、绝对值函数及某些三角函数； 5 进一步完善y 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 期刊。 关键词：m i z a r 机器证明奇函数偶函数周期函数 基于m i z a r 的函数奇偶性及周期性实现研究 青岛科技大学研究生学位论文 o d df u n c n o na n de v e nf u n c n o n a n dp e r l 0 d i cf u n t i o ni nm i z a r t h em a i no b j e c t i v eo fm a t h e m a t i c sm e c h a n i z a t i o ni st ou s ec o m p u t e r st od e d a c e a n d p r o v em a t h e m a f i c a lp r o p o s i t i o n sa n dt h e o r e m s p r e s e n t l y ，m a n yo r g a n i z a t i o n sa r e t a k i n ga c t i v ep a r ti nt h es t u d yo ff o r m a l i z e dm a t h e m a t i c s t h e r ea r em a n yk i n d so f m a c h i n el a n g u a g e ss y s t e mw h i c ha r eu s e dt op r o v em a t h e m a t i c a lt h e o r e m s ，a n d s e v e r a lo ft h e ma r er e c o g n i z e ds u c ha sm i z a r ，p v s ，c o qe t c h o w e v e r ，m i z a rl a n g u a g e s y s t e mh a sd e v e l o p e dr a p i d y ，a n da c c e p t e db r o a da t t e n t i o ni nt h ew o r l d n o w d a y s ， m i z a rh a sa l r e a d yd e v e l o p e dt h em a t h e m a t i ck n o w l e d g et r e a t m e n ts y s t e mi n c l u d i n ga l o to ff u n c t i o n m i z a rm a t h e m a t i c a ll i b r a r yh a si n c l u d e dm o r et h a n1 0 9 0a r t i c l e sa n d a l m o s tc o n t a i n sa l lb r a n c h e so fm a t h e m a t i c s ，e s p e c i a l l yi nt h ef o r m a l i z a t i o no f t o p o l o g yt h e o r e ma n df u n c t i o n a la n a l y s i st h e o r e m s f i r s t l yt h i sp a p e rd e s c r i b e st h eh i s t o r yo fm i z a rs y s t e ma n dt h ew a yt o w r i t e m _ i z a ra r t i c l e s t h e nt h ed e f i n i t i o n so fo d df u n c t i o n ，e v e nf u n c t i o na n dp e r i o d i c f u n c t i o na r eg i v e nw i t ht h em j z a rs y s t e m ，a n dt h ep r o p e r t i e so fo d df u n c t i o n ，e v e n f u n c t i o na n dp e r i o d i cf u n c t i o na r ep r e s e n t e da n dp r o v e dw i t hm i z a r t h em a i nw o r ko f t h i sp a p e ra sf o l l o w s ： 1 t l l ed e f i n i t i o n so fq u a s io d df u n c t i o n ，q u a s ie v e nf u n c t i o n ，o d df u n c t i o na n d e v e nf u n c t i o na r ep r e s e n t e dt h r o u g hm i z a rs y s t e m 2 p e r i o d i cf u n c t i o ni sd e f m e di nm i z a rs y s t e mf o rt h e f i r s tt i m e 3 p r o o f so fo d df u n c t i o n ，e v e nf u n c t i o na n dp e r i o d i cf u n c t i o np r o p e r t i e sa r e c o m p l e t e dw i t ht h em i z a rs y s t e m 4 p r o v e dp r o p e r t i e s o fs o m ef u n c t i o n sb a s e do ng i z a r ，s u c ha st r i a n g l e f u n c t i o n ，a b s o l u t ef u n c t i o n ，s i g nf u n c t i o n 5 d e f m e ds i g nf u n c t i o na n ds h o w e di t sp r o p e r t i e si nm i z a rs y s t e m a l lo ft h ea b o v ec o n t r i b u t i o nh a sp a s s e dt h ec h e c ko fm j z a rs y s t e m ，a n dp u b l i s h e d r l l 基丁m i z a r 的函数奇偶性及周期性实现研究 i nt h ej o u m a lo ff o r m a l i z e dm a t h e m a t i c s ，a n di n c l u d e db yt h em m l ( m j z a r m a t h e m a t i c a ll i b r a r y ) k e yw o r d s ：m i z a r , a u t o m a t e dt h e o r e mp r o v i n g ，o d df u n c t i o n ， e v e n f u n c t i o n , p e r i o d i cf u n c t i o n 青岛科技大学研究生学位论文 目录 摘要i a b s t r a c t i i i 1 绪论1 1 1 机器证明的历史及发展现状 1 2m i z a r 语言系统的历史及发展现状 1 3 课题研究的主要内容 1 4 课题研究的目的和意义 2 函数奇偶性的m i z a r 实现5 2 1 预备知识5 2 2m i z a r 环境部的设置6 2 3 基于m i z a r 的函数奇偶性的研究7 2 3 1 奇函数与偶函数定义的m i z a r 实现7 2 3 2 奇函数与偶函数性质的m i z a r 证明1 3 2 3 3 奇函数与偶函数的复合函数性质的m i z a r 证明1 8 2 3 4 一些初等函数奇偶性的m i z a r 实现2 5 3 函数周期性的m i z a r 实现4 1 3 1 预备知识4 1 3 2m i z a r 环境部的设置4 2 3 3 基于m i z a r 的函数周期性的研究4 3 3 3 1 周期函数定义的m i z a r 实现4 3 3 3 2 周期函数性质的m i z a r 证明4 4 3 3 3 三角函数周期性的m i z a r 证明5 4 3 4 基于m i z a r 的函数周期性论证的检测结果5 8 总结与展望6 1 参考文献6 2 致谢6 5 v 基于m i z a r 的函数奇偶性及周期性实现研究 攻读学位期间发表的学术论文目录6 6 声明6 7 青岛科技人学研究生学位论文 1 绪论 1 1 机器证明的历史及发展现状 机器证明是指使用计算机证明数学定理，也称为定理的机械证明或自动证 明。机器证明是人工智能领域的一个非常重要的分支，也是数学与计算机科学的 一门交叉学科，它的研究与发展已有几十年的历史。早在1 7 世纪，g w l e i b n i z 曾提出“推理机器的设想。1 9 5 6 年由纽厄尔、赫伯特西蒙等人合作编制的逻 辑理论机数学定理证明程序l o g i ct h e o r i s t ( 简称l t ) 使机器证明迈出了逻辑推 理的第一步。1 9 5 8 - - 1 9 6 0 年期间，著名华人数理逻辑学家王浩设计了三个程序， 几分钟之内就证明了该书中一阶逻辑部分的全部定理3 5 0 多条，这项杰出的工作 引起了数学界的轰动，进一步推动了定理机器证明研究的深入发展。1 9 7 7 年，我 国著名的数学家吴文俊教授也涉足这一领域的研究，并在中国科学杂志上发 表了题为“初等几何判定问题与机械化证明”的论文。他提出自己的机械化方法 不仅可以证明许多已知的定理，还能用来发现新的不平凡的几何定理。后来，吴 文俊的这一证明几何定理的新方法被人们称为吴方法，实现了高效几何定理的自 动证明，开创了一个崭新的数学机械化领域 1 - 4 1 。迄今为止，全世界已存在2 9 1 种i s 可用来进行定理证明的机器语言系统，其中有1 5 种数学定理证明系统受到 m k m 协会及大多数专家的认可，譬如a u t o m a t h 系统【6 i 、m l z a r 系统【7 l 、n u p r l 系统 8 , 9 1 和t h e o r e m a 系统【1 0 】等。著名的荷兰数学家f w i e d i j k 在c o m p a r i n g m a t h e m a t i c a lp r o v e r s 1 1 l 中主要从它们知识库的大小、逻辑性表示的强弱和自动智 能的水平三个方面比较h o l 、m i z a r 、p v s 、c o q 1 2 ，1 3 l 等著名的数学定理证明系统， 其中m i z a r 系统由于拥有世界上最大的数学领域知识库，并且在自动智能方面独 立开发出强大的“人机对话”功能，引起世界各国研究机器证明领域人士的广泛 关注。 基于m i z a r 的函数奇偶性及周期性实现研究 1 2m i z a r 语言系统的历史及发展现状 m i z a r 系统是用于证明或计算数学问题的计算机语言系统，它集自然演绎、逻 辑证明、复杂计算、验证排版、科研教学于一身，并拥有自己的编辑语言m i z a l r 语言和世界上最大的数学数据知识库m m l , 同时m m i _ ( m i z a rm a t h e m a t i c a l l i b r a r y ) 也是期刊f o r m a l i z e dm a t h e m a t i c s 的在线版本，可在i n t e m e t 上随时查阅。 m i z a r 语言系统目前大约有3 0 几年的历史，上世纪八十年代初，波兰华沙大学 教授a n d r z e jt r y b u l e c 便设想借助计算机来撰写论文， 1 9 7 3 年在华沙大学图书馆 学和科学信息学院的一次研讨会上，a n d r z e jt r y b u l e c 教授第一次提出要创建一种 可以用来撰写数学论文的计算机语言，并提出这种语言在其功能上应具备以下特 点【1 4 】： 1 具有可存储性和可编译性，即撰写的文章可存储于计算机中，并可将自动 翻译成数学语言： 2 格式整齐匀称且内容简洁易懂； 3 具有自动查找并检验错误的功能； 4 具有方便查找参考文献、删减重复定理的功能： 5 具有自动排版的功能。 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 语言系统，同时用其编辑并成功运行了第一 组数学定理，这样，m i z a r 语言系统正式诞生了。1 9 7 5 年在波兰科学协会的支持 下，m i z a r 语言系统得以进一步研究。同年1 1 月a n d r z e jt r y b u l e c 教授提交了m i z a r 语言系统的最初版本m 娩a 卜p c ( p c 表示命题演算) ，并且预见性的提出了数 学数据库的问题，也就是后来的m i z a rm a t h e m a t i c a ll i b r a r y ( 简称m m l ) 。 1 9 7 7 年m i z a r 系统实现了由m i z a r p c 到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 ) 的艰难进化，并完成了将系统发展成为m i z a r - q c 6 0 0 0 的目标。1 9 7 8 年m i z a r 系 统在语义和句法方面做了大量地充实和改进，新定义了谓词( p r e d i c a t e ) 、结构 ( s c h e m e ) 、预声i j y j ( 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 ) 等 概念，并在m i z a r 系统下首次对函数和关系进行了定义。1 9 7 8 1 9 8 1 年期间，m i z a r 系统完成了从m i z a r - f c 到m i z a r - 2 的升级，并且在m i z a r 论文中设置了环境部， 使文章的内容更加清晰和规范。1 9 8 3 1 9 8 8 年，m _ i z a r 先后实现了m i z a r - h p f 和 m i z a r - 4 的历史性的突破。现在所用版本就是从逐步升级的m i z a r - 4 系统演化而来 的【1 5 1 。 2 青岛科技大学研究生学位论文 1 9 8 9 年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 lr e s e a r c h 的资金支持。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 si n m i z a r ) 完成【1 6 1 。 到目前为止，m i z a r 语言系统已经发展到7 1 1 版本，数据库( m m l ) 内含 1 0 9 0 多篇文章，2 万多个数学定义。这些数学知识几乎涵盖了数学的每一个分支， 如代数、数学分析、图论、几何学、范畴理论、数论等领域。 1 3 课题研究的主要内容 自1 9 8 9 年l m z a r 语言系统建立以来，数据库m m l 不断得到充实，其中收录了来 自波兰、加拿大、中国、日本等多个国家的教授学者和研究生撰写的数学论文【1 0 1 。 m 娩a r 数据库m m l 涉及了数学领域中的多个学科，但关于奇偶函数及周期函数的 定义和性质等还没有涉及。本文的主要研究内容如下： 1 在l 、j _ i z a r 语言系统下，给出推广了的拟奇函数、拟偶函数、奇函数、偶函 数及周期函数的定义； 2 基于该系统下函数的性质，给出了奇函数、偶函数及周期函数性质的m i z a r 论证： 3 在l 、j i z a r 系统下实现了正弦函数、余弦函数、正切函数、余切函数等三角 函数和某些特殊函数的奇偶性和周期性的论证。 本文主要通过运用m i z a r 语言给出奇函数、偶函数及周期函数的定义法，实现 了奇偶函数及周期函数相关定理的m i z a r 论证，完成了数学理论的m i z a r 语言转化。 1 4 课题研究的目的和意义 目前，u i z a r 系统已经发展成为包括语言的开发、数据库的扩充、自动推理能 力的提高及翻译形式的多样化处理等多方面内容的庞大的语言系统。 本课题的研究是基于对机器证明和数学定理自动推理系统m i z a r 及其语义、 语法的深刻理解，在m i z a r 系统中利用其庞大的数学数据库( m m l ) ，对分析学中 的奇函数、偶函数及周期函数做了细致的研究和讨论，通过对这一理论的研究和 3 基丁m i z a r 的函数奇偶性及周期性实现研究 探索，不仅扩充了m i z a r 数据库，同时也使数据库中的知识储备更加系统和完备， 为后续定理的证明和分析学中大量问题的m i z a r 语言实现及解决奠定了基础。 4 青岛科技人学研究生学位论文 2 函数奇偶性的m i z a r 实现【j 8 埘】 到目前为止，在m i z a r 语言系统的数据库中有关奇函数和偶函数的定义及性 质的相关知识还没有涉及。因此这部分内容在m i z a r 语言系统中尚有很大的扩展 空间，函数奇偶性的m i z a r 语言实现对于充实m i z a r 数据库以及进一步研究函数的 其他性质都有很重要的意义。 2 1 预备知识 本节简要介绍一些相关的定义和性质。 定义2 1 1 【1 7 l 设函数厂( 砷的定义域为d ，其中d 关于原点对称，即 x d ，x d ， 若厂( 叫= 厂( 力，v x d 则称厂( 力为偶函数；若厂( 一功= 一厂( 力，v x d ，则称，( 功 为奇函数。 定义2 1 2 设函数厂( 力的定义域为d ，若z d 且一x d 就有厂( 卅= 厂( 功， 则称，( 砷为拟偶函数；若x dj j - x d 就有，( 一功= - f ( x ) ，则称厂( 功为拟奇 函数。 性质2 1 1 函数厂( 功与函数g ( 砷定义域相同，若厂( 力与g ( 力都是偶函数， 则，( 砷g ( 功也是偶函数。 性质2 1 2 函数，( 功与函数g ( 功定义域相同，若，( 矽与g ( 力都是奇函数， 则f ( x ) g ( x ) 是偶函数。 性质2 1 3 函数厂( p 与函数g ( 砷定义域相同，若厂( 力与g ( 砷一个是偶函数 另一个是奇函数，则f ( x ) g o ) 是奇函数。 性质2 1 4 函数厂( 矽与函数g ( 砷定义域相同，若厂( 力与g ( 力都是偶函数， 且在定义域内有g ( 功0 ，则f ( x ) g ( x ) 是偶函数。 性质2 1 5 函数，( 功与函数g ( 砷定义域相同，若，( 力与g ( 力都是奇函数， 且在定义域内有g ( 功0 ，则f ( x ) g ( x ) 是偶函数。 5 基t - m i z a r 的函数奇偶性及周期性实现研究 性质2 1 6 函数厂( 砷与函数g ( 力定义域相同，若，( 力与g ( 力一个是偶函数 另一个是奇函数且在定义域内有g ( 力0 ，则厂( x ) g ( x ) 是奇函数。 奇偶函数还有许多性质，这里不再一一介绍了，以上几个性质主要参考了 文献【1 8 p 1 。 2 2m 泣a r 环境部的设置 1 v l i z a r 论文的开始部分需要设置环境部( e n v r i o n ) ，为主体部分对数学问题的 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 sn u m b e r s ， r e a l _ i ，x c m p l x0 ，o r d i n a l l ， a r y t m1 ，s o b s e t j ，r e l _ 吼1 ，x b o o l e _ 0 ，m e m b e r e d ，p a r t f u n l ， f u n c t j ，a b i a n , t a r s r d , a r y t m3 ，c a r d _ i ，c o m p l e x i ，v a l u e d _ i ， s o u a r e _ i ， a b s v a l u e ，x r b 吐：0 ，x 泓1 10 ， e u c l i d ，s i n _ c o s ， s i n _ c o s 2 ，x x r e a l _ i ，s i n _ c o s 9 ，s i n _ c o s 4 ，f u n c t8 ； n o t a t i o n s c o m p l e x l ，x c m p l x _ 0 ，o r d i n a l l ，n u m b e r s ， x r e a l _ 0 ，x x r e a l _ 0 ，r e a l 一1 ，m e m b e r e d ，a b s v a l u e ，p a r t f u n l ， t a r s k i ，x a o o l e _ 0 ，s u b s e t _ i ，e u c l i d ，r e l 幔1 ，f u n c t _ i ，f u n c t _ 2 ， s i n _ c o s 2 ， s i n _ c o s ，v a l u e d _ i ，r c o m p _ i ，s q u a r e _ i ，s i n _ c o s 9 ， r e l s e t _ i ，f d i f f9 ； c o n s t r u c t o r s r e a l _ i ，s u p i n f _ i ，r c o m p 一1 ，s e q _ i ，e u c l i d ， s q u a r e _ i ，l i m f u n c l ，a b s v a l u e ，s i n _ c o s 2 ，r e a c t1 ，r e l s e t _ i ， n u m b e r s ，m e s f u n c l ，s i n _ c o s 9 ，b i n o p ，s i nc o s ，c o m p l e x l ， f i n s e q _ 4 ，p a r t f u n 2 ，p a r t f u n l ，f d i f f9 ，f d m f - 1 ，v a l u e d _ l ； r e g i s t r a t i o n s x x r e a l0 ，x r e a l _ 0 , x b o o l e _ 0 ， m e m b e r e d ， x c m p l x _ 0 ，n u m b e r s ，v a l u e d _ 0 ，f t m c t _ i ，r e 咀1 ，f t r n c t2 ， r e l s e t _ i ； r e q u i r e m e n t sr e a i ，n u m e r a ls ，s u b s e t , a r i t h m ，b o o l e ； 6 f l 青岛科技人学研究生学位论文 d e f i n i t i o n sc o m p l e x l ，s i nc o s 4 ，x r e a i ，0 ，a b s v a i ，i e ，i n t1 ， h j n c t1 ，r e l s e t1 ，r f in 虹玎2 ，p r o b1 ，x b o o l e0 ，e u c l l d ，r c o m p1 ， t a r s k i ，p b o o l e ，v a l u e d1 ，m e s f u n c l ，s i nc o s ，s i nc o s 2 ，r f u n c r1 ， n u m b e r s ，s i n _ c o s 9 ，f i n s e q _ 4 ，x c m p l x0 ，u m n j n c l ，s q u a r e _ i ， s u b s e t1 ，r e 乙气t1 , m e m b e r e d ，p a r t f u n 2 ，p a r t f u n l ，f d i f f9 ，f d e f f1 ， v a i ，i e d0 ，s e q m3 ： t h e o r e m ss i nc o s 4 ，x r e a i ，o ，a b s v a i ，i 甩，i u n c t2 ，c o m p l e x l ， o o l e9 ，e u c l l d ，x c m p l x1 ，s i nc o s 9 ，x 通a l1 ，v a l u e d1 ， x b o o l e1 ，s i nc o s ，s i nc o s 2 ，r f u n c t1 ，x c l x0 ，r e l a tl ， n r 1 r i u n 2 ，r 玎驱玎1 ，t a r s k i , n 讯1 1 阿n 1 ，n u m b e r s ； s c h e m e sf i 腻c i 2 ： 最后还要强调的是：由于本文给出了一些新的定义，所以在环境部的词汇 v o c a b u l a r i e s 中就需要添加本文的名字f u n c t8 。 2 3 基于m i z a r 的函数奇偶性的研究 环境部设置完成之后，接着就是正文的书写了。每篇m i z a r 文章的正文只有 一个部分，以“b e g i n 开始，一般情况后面接跟一个变量预先声明模块来声明后 面论证过程中将要用到的某些或全部的变量的类型。以下是本文的变量预声明： r e s e r v ex ，rf o rr e a l ： 放在正文的开始部分，事先声明数据的类型。例如：“r e s e r v ex ，rf o rr e a l ” 声明x ，r 为实数，也就是除了重新声明，在下文任何位置出现的x ，r 都是实数， 若开头没有预先设定属性，则每次用到字母时，都必须特别指明。对于没有标明 属性的字母，即在“r e s e e f o r 部分和出现该字母的定义或定理中都没有设 定其属性的字母，m i z a r 系统是不承认其存在的合理性的。特别注意的是字母的 属性对“r e s e r v e f o r 的选取是满足就近原则的。 2 3 1 奇函数与偶函数定义的m i z a r 实现 在m i z a r 语言系统中，为了方便以后的引用，通常将定义范围尽量扩大，为此 将原有的实数范围内的奇偶函数的定义扩大到复数范围内，本节首先给出了对称 集的定义，然后给出拟奇函数和拟偶函数的定义，最后依据以上定义给出奇偶函 数的定义，这样就将奇函数和偶函数的定义推广了。 由于m j z a l 系统的严谨性，所以为了给出奇函数与偶函数的定义，首先要给 7 基于m i z a r 的函数奇偶性及周期性实现研究 出对称集的定义。 d e f i n i t i o n l e tab es e t ： a t t rai ss y m m e t r i c a lm e a n s ：f u n c t 一8 ：d e f 1 f o rxb e i n gc o m p l e xn u m b e rs txi na h o l d s xi na ： e n d ； 为了更好的理解这个定义过程，下面简要介绍一下m i z a r 语言系统中语句的 含义及其使用方法， l 、l e t 语句 l e t 语句也是用来说明数据类型的，由于前面没有用r e s e r v e 语句来规定定 义中a 的类型，所以在定义中需要用l e t 语句来说明a 代表一个集合，在这里 r e s e r v e 语句与l e t 语句的作用是一致的，只是所放的位置不同而已。 2 、a t t r 语句 a t t r 是用来定义数据属性的，是不需要证明其存在性及唯一性的。 3 、f o r h o l d s 语句 f o r h o l d s 语句在m i z a r 系统中使用频率极高，主要有以下三种表述形式： ( 1 ) 一般的定理表述 f o rxb es e th o l d sp ( x ) ，即对于任意一个集合x ，能推出结论p ( x ) 成立。 f o rxb es e ts tq ( x ) h o l d sp ( x ) ，即对于任意一个集合x ，如果满足条件q ( x ) ， 就能推出结论p ( x 1 成立。 ( 2 ) 含存在性的定理表述 f o rxb es e ts tq ( x ) h o l d se xys tp ( x ，y ) ，即任给集合x ，如果满足条件q ( x ) ，就 能推出存在y ，使得结论e ( x ，y ) 成立。 另外，f u n c t8 ：d e f1 代表f u n c t8 这篇文章的第一个定理，有了这个标号 后可以方便以后的引用。 从上面的m i z a r 定义中可以看出，a 是对称的集合的含义是：对于任意的复 数x ，如果x a 就有一x a 。 上面所定义的对称集既有对称的复数集又有对称的实数集，所以以 “r e g i s t r a t i o n 的形式证明其合理性。以后引用时，m i z a r 系统就会默认其正确性， 避免重复证明的麻烦。 r e g i s t r a t i o n d u s t e rs y m m e t r i c a ls u b s e to fc o m p l 2 2 q 8 青岛科技人学研究生学位论文 e x i s t e n e e p r o o f t a k e # c o m p l e x ； l e txb ec o m p l e xn u m b e r ； t h u st h e s i sb yx c m p l x _ 0 ：d e f2 ： e n d ； e n d ； r e g i s t r a t i o n c l u s t e rs y m m e t r i c a ls u b s e to fr e a l ； e x i s t e n c e p r o o f t a k e 【撑】呲 l e txb ec o m p l e xn u m b e r ； f o r xs t xi nr e a l h o l d s xi nr e a l ； h e n c et h e s i s ； e n d ； e n d ； 这里用到了m i z a r 定义中常见的一种语句刊u s t e r 语句。它实质是一种声 明，通常在两种情况下会使用到它： 一是对某种模式m o d e 赋予某种属性( 撒曲u t e ) ，复合为一个新的模式，然后 对这种新模式的存在性给出声明，如： d e f i n i t i o n c l u s t e rs y m m e t r i c a ls u b s e to fr e a l ； e x i s t e n c e p r o o f e n d ； e n d ； 上述证明属于这种情况。 二是声明两种模式的隶属关系。证明这种情况时，只需证明一致性，如后面 出现的符号函数： r e g i s u a t i o n l e txb er e a ln u m b e r ； 9 基于m i z a r 的函数奇偶性及周期性实现研究 d u s t e rs i g n u m x - r e a l ； c o h e r e n c e p r o o f e n d ； e n d ； 在m i z a r 系统中无论是存在性、唯一性还是一致性的证明都是以p r o o f 开始， e n d 结束的，中间部分是证明过程。 有了前面的注册后，便可以在这里声明a 为对称的复数集的子集，即： r e s e r v eaf o rs y m m e t r i c a ls u b s e to fc o m p l e x ； 以下是m i z a r 下对称定义域的关系的定义 d e f i r t i t i o n l e trb er e l a t i o n ； a t t rri sw i t h _ s y m m e t r i c a l _ d o m a i nm e a n s ：f u n c t _ 8 ：d e f2 d o mri ss y m m e t r i c a l ； e n d ； 同时注册空集属于带有对称定义域的一种关系 r e g i s t r a t i o n c l u s t e re m p t y 一 w i t h _ s y m m e t r i c a l _ d o m a i nr e l a t i o n ； c o h e r e n c e p r o o f a i ： 】i ss y m m e t r i c a l p r o o f 青岛科技大学研究生学位论文 设结论不成立，最后推出矛盾。 r e g i s t r a t i o n 1 e trb ew i t h _ s y m m e t r i c a l _ d o m a i nr e l a t i o n ； c l u s t e rd o mr 一 s y m m e t r i c a l ； c o h e r e n c eb yd e f 2 ； e n d ； 以上两个c l u s t e r 语句都是声明隶属关系，所以只需证明一致性，且f l c o h e r e n c e 。 另外证明中所用的b v 是为了说明结论成立的理由的，这些理由可以是本文中的定 义和定理，也可以是已经收录在m m l 中的a b s t r a c t 中的定义及定理。 m i z a r 系统下拟偶函数与偶函数的定义的实现过程如下： d e f i n i t i o n l e tx yb ec o m p l e x - m e m b e r e ds e t ； l e t f b e p a r t f u n c o fx ，y ； a t t rfi sq u a s i _ e v e nm e a n $ ：f u n c t 一8 ：d e f 3 f o rxs txi nd o mf xi nd o mfh o l d sf ( - x ) = f x ； e n d ； d e f i n i t i o n l e t ) ( ，yb ec o m p l e x m e m b e r e ds e t ； l e tfb ep a r f u n co fx ，y ； a t t r f i se v e n m e a n s f u n c t 一8 ：d e f 4 fi sw i t h _ s y m m e t r i c a l _ d o m a i nq u a s i _ e v e n ； e n d ； 从以上两个定义可以看出拟偶函数与偶函数的主要区别在于定义域是否对 称，这样既给出了偶函数的定义，又将其加以推广。 r e g i s t r a t i o n l e tx , yb ec o m p l e x m e m b e r e d s e t ； d u s t e rw i t h _ s y m m e t r i c a l _ d o m a i nq u a s i e v e n 一 e v e np a r t f u n co fx , y ； c o h e r e n c eb yd e f 4 ； d u s t e re v e n - w i t h _ s y m m e t r i c a l _ d o m a i nq u a s i _ e v e np a r t f t m co fx y ； c o h e r e n c e b yd e f 4 ； 1 1 基于m i z a r 的函数奇偶性及周期性实现研究 e n d ； 为了将问题更加清晰化，这里又给出函数在某个集合上是偶函数的定义： d e f i n i t i o n l e t a b es e t ； l e t ) 【，yb ec o m p l e x m e m b e r e ds e t ； l e tfb ep a r t f u n co f x y p r e dfi s e v e n o nam e a n s ：f u n c t8 ：d e f5 ac = d o mf & f 陋i se v e n ； e n d ； 在m i z a r 里，p r e d 是用来定义谓词( p r e d i c a t e s ) 的，谓词定义实际上是为了定义 一种表达性的术语，也是不需要证明其存在性和唯一性的，在系统中检验正确后 就可以直接使用。 类似的，给出拟奇函数、奇函数和在某个集合上是奇函数的定义，如下： d e f i n i t i o n l e tx yb ec o m p l e x - m e m b e r e ds e t ； l e tfb ep a r t f u n co f ) ( ，y ； a t t rfi sq u a s i _ _ o d dm e a n s f u n c t 一8 ：d e f 6 f o rxs txi nd o mf & xi nd o mfh o l d sf ( - x ) _ - f x ； e n