（应用数学专业论文）一元函数高阶导数在mizar语言系统下的实现研究.pdf

青岛科技大学研究生学位论文 一元函数高阶导数在m iz a r 语言系统下的实现研究 摘要 数学问题的计算机证明也称数学机械化，是指用计算机证明、推理计算数 学问题。m i z a r 语言系统是由波兰华沙大学的a n d r z e jt r y b u l e c 教授为首的数学 家和计算机专家在上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的 计算机语言系统。该系统如今拥有自己的数据库删l ，其中收录了几乎涵盖了数 学各个分支的1 0 0 0 多篇数学论文，并且还解决了像连续格的证明、j o r d a n 曲线 及b r o u w e r 不动点等定理，这类人们用手无法计算和证明的复杂问题。同时，它 在自动化控制、声音和图像识别等研究领域也有着广泛的应用。 本文首先介绍了m i z a r 语言系统的发展历史，其次给出了在该系统下证明和 自动校验数学命题的方法，在此基础上针对一元函数高阶导数的不同问题，给出 了相应的m i z a r 算法。作者的主要工作如下： 1 在m i z a r 语言系统下给出了几类一元函数高阶导数公式的实现方法； 2 实现了广义指数函数的m i z a r 语言定义方法，证明了其复合函数的可微 性定理并推导了其高阶导数公式； 3 给出了推导初等函数、超越函数和复合函数n 阶导数公式的m i z a r 语言 算法，并给出了应用说明； 4 验证了函数高阶导数的运算法则及其定理的m i z a r 语言实现方法，并给 出了简要的应用说明。 以上结果均已通过m i z a r 语言系统的验证，被收录在m i z a r 数据库删l 中。 关键词：m i z a r 语言系统计算机证明高阶导数n 阶导数 青岛科技人学研究生学位论文 t h ef u n c t l 0 nh i g h e rd i f f e r e n t i a l i nm i z a rl a n g u a g ep r o j e c t a b s t r a c t t 1 1 ec u m p u t e rc a l c u l a t o ro fm a t h e m a t i c sp r o b l e mb e i n ga l s oc a l l e dm a t h e m a t i c s m e c h a n i z a t i o n ，i st o u s eac u m p u t e rt o p r o v ea n dd e d u c ec a l c u l a t i o nm a t h e m a t i c s p r o b l e m m i z a r1 a n g u a g ep r o j e c ts t a n e d8 0 si n l a s tc e n t u 巧i sac o m p u t e r l a n g u a g e p r o j e c tw h i c hi su n d e rt h el e a d e r s h i po fa n d r z e j7 r r y b u l e ca tt h ep l o c ks c i e n t i f i c s o c i e t y ；p o l a n dw h of o u n d e dt h el a n g u a g ep r i ) j e c t w i t ht h ef u n c t i o no fp r o v i n g ， v e r i f y i n g a n dt y p e s e t t i n g t b d a ym i z a r l a n g u a g ep r o j e c t h a sal a r g em i z a f m a t h e m a t i c a ll i b r a r v ，e m b o d y i n gm o r et h a n1 0 0 0a n i c l e sw h i c ha l m o s tc o n t a i n sa l l b r a n c h e so fm a t h e m a t i c s ，a n ds o l v e st h ef o 珊a l i z a t i o no fc o n t i n u o u sl a t t i c e st h e o r e m ， j o r d a n sc u et h e o r e ma n db r o u w e rf i x e dp o i n tt h e o r e mw h i c hm a t h e m a t i c i a nc a n n o t s o l v e db yh a n d i ta l s oa p p l e si nm a n yf i e l d ss u c ha sa u t o c o n t r o l ，v o i c e ，i m a g e i d e n t i f i c a t i o ne t c ，a n ds e t sag o o df o u n d a t i o nt om a t h e m a t i c sa n dt h er e l a t e dm a j o r t h i sd i s s e r t a t i o nd e s c r i b e st h eh i s t o r yo fm i z a rl a n g u a g ep r o j e c ta n dt h em e t h o d o fp r o v e i n ga n da u t o m a t i ci d e n t i f i c a t i o n f i r s t l yi no r d e rt oc a r r yo u tt h ec a l c u l a t o ro f m a t h e m a t i c sp r o b l e m，w es h o u l d西v et h em e t h o do fm a t h m a t i cd e d u c t i o na n d c a l c u l a t o rw h i c hc a nb ei d e n t i f i e da n di d e n t i f i c a t e db yc o m p u t e r ：d i s c u s st h er e a l i z a t i o n o ft h eh i g h e rd i f 诧r e n t i a lf b n n u l ao fa ( 1 0 l l a r ，a n dp r o v es o m ep r o p e n i e so ft h eh i g h e r d i f ! f e r e n t i a lf o 唧u l ao fad o l l a ru n d e rt h i ss v s t e 咖t l l l ea u t h o r sm a i nw o r ka sf b l l o w s ： 1 c a 玎vo u tt h eh i g l l e rd i f f e r e n t i a lf o 咖u l ao faf e ws p e c i a lf u n c t i o n su n d e rm i z a r l a n g u a g ep r o j e c t ； 2 d e f i n ee x p o n e n t i a lf u n c t i o n ，a n dg i v eh i g h e rd i f f e r e n t i a lc a l c u l u sf b n n u l aa n d d i f f e r e n t i a b l et h e o r e m so fs o m ec o m p o s i t ef u n c t i o n sa b o u te x p o n e n t i a lf u n c t i o n ； 3 i n d u c ea n dd e d u c en t hd i f f e r e n t i a lc a l c u l u sf o r m u l a0 fe l e m e n t a r vf u n c t i o na n d s p e c i a lc o m p o s i t ef u n c t i o n s ，a n di n t r o d u c et h ea p p l i c a t i o na b o u tt h e m ； 4 p r o v es o m ea l 擘r o r i t h m sa n dp r o p e n yo fh i g l l e rd i f ! f e r e n t i a lc a l c u l u sf 0 咖u l a ， a n di n t r o d u c et h ea p d l i c a t i o na b o u tt h e mb r i e n v t h ea u t o m a t i cr e a s o n i n ga n dp r o v i n gp r o c e s s ，w h i c hi sr e l a t e dt ot h ea b o v e a s p e c t s ，h a v eb e e nc o m p l e t e da n dv e r i f i e dt ob ec o r r e c ti nm i z a rl a n g u a g ep r o j e c t 1 l l 一元函数高阶导数在m i z a r 语言系统下的实现研究 l 【e yw o i t d s ：m i z a rl a n g u a g ep r l d j e c t ， a u t o m a t e dt h e o r e mp r o v i n g ， h i g h e r d j 伍b r e n t i a l ，n t hd i f ! f e r e n t i a l 青岛科技大学研究生学何论文 1 绪论 1 1 数学问题计算机证明的历史及发展现状 机器证明( a t p ：a u t o m a t e dt h e o r e mp r o v i n g ) 是使用计算机证明定理，也称 为定理的机械证明或自动证明。它是人工智能领域的一个重要分支，也是数学与 计算机科学的一门交叉学科，它的研究与发展至今约有5 0 年的历史。1 9 5 6 年由 纽厄尔、赫伯特西蒙等人合作编制的逻辑理论机数学定理证明程序l o g i c t h e o r i s t ( 简称l t ) 使机器证明迈出了逻辑推理的第一步。之后，美籍华人学者、 洛克菲勒大学教授王浩在“自动定理证明”上获得了更大的成就，他用他首创的 “王氏算法”在一台速度不高的i b m 7 0 4 电脑上，不到9 分钟就把在数学史上视 为里程碑的著作数学原理中的全部( 3 5 0 条以上) 定理证明了一遍，被国际 公认为机器定理证明的开拓者之一。1 9 7 7 年我国著名数学家吴文俊院士在中国 科学杂志上发表了题为“初等几何判定问题与机械化证明 的论文，提出了一 种新的证明等式型初等几何定理的代数方法( 也称为“吴法”) ，实现了高效几 何定理的自动证明，开创了一个崭新的数学机械化领域。机器证明及其应用是我 国攀登计划项目之一，该项目的核心内容主要是几何定理的机器证明和非线性代 数方程组理论、算法和应用。目前，在几何定理机器证明方面，我国处于国际领 先地位。在非线性代数方程组研究领域，我国已进入先进行列，但目前还不能说 领先 卜4 。 近几年来，一些计算机辅助处理的数学系统备受人们的关注，如a u t o m a t h 、 t h e a x 、e l f 、m i z a r 、h o l 、l e g o 、i m p s 和a l f 等系统。它们各自的初衷不同，却 有一个共同的特征：人类使用机器语言书写、计算、推理和证明文本性质的数学 问题，并使用机器验证其正确性 5 6 。 1 2m iz a r 语言系统的历史和发展现状 m i z a r 语言系统是一种计算机语言系统，是在定理自动证明的发展过程中产 生并且发展起来的一个专门用来构建m i z a r 数学知识库的自动推理校验系统。目 前，m i z a r 语言系统拥有世界上最大的数学数据库( m m l ) ，同时此数据库也是期刊 凡i r m 口f f z 耐 缸咖p 脚口矗体的o n li n e 版本，在i n t e r n e t 上可随时查阅 7 。 m i z a r 语言系统的历史可以追溯到上世纪八十年代初，当时波兰华沙大学教 一元函数高阶导数在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 教授第一次完整地提出了 一种可实现的用来撰写数学论文的计算机语言，并对这种语言在其功能上的一些 必需的特点作了说明 8 ： 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 n m 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 iz a r 语言系统的初级版本叫iz 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 7 1 9 8 8 年期间，研究人员对m iz a r p c 进行了大量的语法和句法改进。 尤其是在1 9 7 8 年m i z a r p c 有了2 次重大的改进：一、定义了谓词、结构、预声 明、绝对相等的概念，使得很多命题不需要讨论就能实现系统的自行验证；二、 给出了函数的定义和关系及其运算的定义。在这期间，m i z a r 语言系统还成功实 现了5 次版本的升级，并最终实现了其在不同操作系统下的成功运行 7 。 1 9 8 9 年删l 开始投入使用，并且随着删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 册口舷以胁咖删口行岱得到了美国0 f f i c eo fn a v a l r e s e a r c h 的资金支持。2 0 0 2 年，m i z a r 数学百科全书e 删( 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 ) 完成 7 。 到目前为止，m i z a r 语言系统已经发展到7 8 版本，m m l 为4 7 2 版本，内含 1 0 0 0 多篇文章，2 万多个数学定义，将近4 0 万条定理 9 。并且已经形成了系统 化的数学知识领域，这些数学知识几乎涵盖了数学的每一个分支，如数学分析学、 代数学、几何学、数论、图论、范畴理论等领域。特别是在对连续格的证明及j o r d a n 曲线、b r o u w e r 不动点等定理的证明中，解决了一些人们用手无法计算和证明的 复杂问题，从而显示了m i z a r 语言系统的优越性。同时，它在自动化控制、声音 和图像识别等研究领域也有着广泛的应用。 2 青岛科技大学研究生学位论文 1 3 课题研究的主要内容 自1 9 8 9 年m i z a r 语言系统完全建立以来，数据库删l 不断得到充实，其中收录 了来自波兰、日本、中国、加拿大等多个国家的教授学者和研究生撰写的数学论 文 1 0 。m i z a r 数据库硎l 涉及了数学领域中的多个学科，但关于一元函数的高阶 导数及函数高阶导数的运算法则和性质等还没有涉及。本文的主要内容如下： 1 在m i z a r 语言系统下，给出了推导三角函数、幂函数、对数函数、反函数、常 用函数和复合函数高阶导数公式的新算法； 2 基于该系统中函数的定义，给出了广义指数函数m i z a r 语言的定义方法，并且 还给出了复合函数可微性定理及其高阶导数公式的m i z a r 语言实现方法； 3 归纳推导了正弦函数、余弦函数、对数函数、幂函数、常数函数和常用函数 的n ( ，7 一+ ) 阶导数公式的m i z a r 语言实现，并且介绍了n 在指定阶数下的 应用方法； 4 在函数n ( 力一十) 阶导数公式实现的情况下，使得函数高阶导数的运算规 律和性质的m i z a r 语言算法得以实现，并对运用这些算法给出了说明。 本文主要通过运用m i z a r 语言给出函数高阶导数公式、运算规律和性质新算 法盼方法，实现了相关定理的m i z a r 语言论证，完成了数学理论的m i z a r 语言转化。 1 4 课题研究的目的和意义 本课题的研究是在对数学问题的计算机证明和数学定理自动推理系统m i z a r 及其语义、语法深刻理解的基础上，在m i z a r 语言系统中利用其语言及庞大的数 学数据库( m m l ) ，对分析学中的理论与方法做的进一步的研究和应用。通过对 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 语言的开发、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 的翻 译机制，增强 l i z a r 语言系统的逻辑推理和校验纠错能力，加强与其他机器证明 3 一元函数高阶导数在m i z a r 语言系统下的实现研究 工具的交叉研究和相互转化。m i z a r 语言系统的发展需要庞大的数学领域知识库 ( 删l ) 的支持，数学学科的发展也将推动数学定理自动证明m i z a r 语言系统的发 展。 4 青岛科技大学研究生学位论文 2miz a r 语言系统概述 2 。1m iz a r 语言系统简介 m i z a r 语言系统主要由三部分组成：一是m i z a r 语言，它帮助数学家使用机器 识别的语言撰写数学论文；二是m i z a r 软件，它收集整理数学论文和检验数学论 文的正确性与否；三是m i z a r 数据库，它是世界上可以被计算机检验和处理的最 大的数学知识数据库 1 1 。通过使用m i z a r 语言来定义、计算、推理和证明的数 学定理，称为m i z a r 文章，并可利用m i z a r 本身提供的软件在p c 机上对其进行验证。 通过验证的m i z a r 文章将会被收录到m m l 数据库中，并发表在波兰的f o r m a l i z e d m a t h e m a t i c s 杂志匕。 2 2m iz a r 语言系统的安装 m i z a r 语言系统可以安装到下列操作平台： f r e e b s d ( i 3 8 6 ) ，d a r w i n m a c o s x ( p p c ) ，w i n 3 2 ，l i n u x ( i 3 8 6 ) ，s o l a r is ( i 3 8 6 ) ， a n d l i n u x ( p p c ) 。 无论在单机还是在网络环境中，m i z a r 语言编写出来的程序都可以直接移植 到其他机型上去使用。 2 2 1 安装过程 随着系统版本的更新升级，安装也越来越简单。下面介绍在w i n d o w s 系统 下的安装程序： s t e p1 ：在p c 的d 盘上新建一个文件夹，命名为m i z a r s y s ； s t e p2 ：从垫主主乜；么纽i 圣垒! ：q ! g 么兰y 兰主皇堡么i 翌鱼旦墨：b 主堡! 苎鱼q 塑翌! q 鲴的页面中找到 w i n 3 2 r e l e a s e s ：主卫；么么堡i 圣垒! ：坚! 堡：旦型坚：乜! 么巳堕鱼么苎y 墨主皇虫么i 墨垒鱼二! i 旦墨垄么， 单击f t 巳：m i z a r u w b e d u 乜1 巳u b s y s t e m i 3 8 6 一w i n 3 2 ，然后在打丌 的页面中找到最新版本，并且复制新版本； s t e p3 ：将新版本粘贴到新建的文件央m i z a r s y s 下，双击解压缩； s t e p4 ：打开命令提示符，进入d 盘，输入c d ：m i z a r s y s 回车，再输入i n s t a l l d ：m i z a r 回车，等待数秒安装即可完成。 2 2 2 改变操作路径 右键单击我的电脑，然后依次点击“属性”“高级”“环境变量 ，在 “环境变量”里双击p a t h ，最后在p a t h 里加入d ：m i z a r ，即可完成对操作路 径的改变。 5 一元函数高阶导数在m i z a r 语言系统下的实现研究 2 3m iz a r 语言的数据类型 在m i z a r 语言系统中，每一个变量都有他们自己的数据类型。在书写m i z a r 文章时必须声明所使用的变量是删l ( m i z a r 数据库) 中的哪一种数据类型。新 的数据类型可以通过s t r u c t u r e 、m o d e 、a t t r 和c l u s t e r 等定义而得到。一般情 况下可以通过预先声明的方式来声明变量的类型。当然变量类型也可以是来自其 它类型的参数，类型符号与参数之间通过关键词“o f ”来体现，如： s u b s e t o fx ，e l e m e n to fd ， f u n c t i o no fx ，y 。 如果在书写文章的过程中要用到没有预先声明的变量，则应该在定理陈述中 明确指出它的类型，否则系统将不承认其存在的合理性。 m i z a r 中基本的数据类型是在文件h i d d e n 中，它会自动加到每一篇m i z a r 文 章。这些自动加入的数据类型我们称之为内置类型，主要包含以下几种数据类型： a n y ， s e t ， e 1 e m e n to fx ， d o m a i n ， s u b s e to fd ，s u b d o m a i no fd ， r e a l ， n a t 等。 a n y 是范围最大的一个数据类型，其它的类型都可以扩大到a n y 类型；s e t 类型和a n y 类型是等价的；d o m a i n 类型表示非空集合；s u b d o m a i n 类型是d o m a i n 类型的子集；r e a l 代表实数类型；n a t 表示自然数。 2 4miz a r 语言的基本表达符号和命题表述词汇 2 4 1m iz a r 语言的基本表达符号 m i z a r 语言的符号是基于纯粹的数学符号、该符号的英文表述和一般的a s c i i 字符相结合的原则来定义和编写的。举例如下： 普通数学命题中v js n u f 2 j c 争 的逻辑符号 m i z a r 语言系统中 f o re x = 屈，口2 2 ，口- 卢n 彤； e n d ； 其中，x 是新定义的结构名，a 。，口：，a 。是函子名，函子可以是新定义的， 1 0 青岛科技大学研究生学位论文 也可以引用m i z a r 数据库中定义过的，。，卢：，卢。是对应函子的属性类型。如 m i z a r 中基于1 s o n e d 结构的名为m a n v s o n e d 的结构，就是由一个函子s o n s 支撑建 立的，其在m i z a r 中的定义表述为： d e f i n i t i o n1 e tsb e1 s o r t e d ：1 s o r t e d 是一个结构 s t r u c tm a n y s o r t e do v e rs s o n s - m a n y s o n e d s e to ft h ec a r r i e ro fs 彬； e n d ： 其中，函子s o r t s 的属性是m a n v s o n e d s e to ft h ec a i e ro fs 。 2 5 8 重新定义( r e d e f i n i t i o n ) 重新定义，是指对于删l 中已存在的谓词定义( p r e d i c a t e s ) 、算子定义 ( f u c t o r s ) 、模式定义( m o d e s ) 和属性定义( a t t r i b u t e s ) ，在不改变原定义符号的 前提下，改变其定义后的数据属性或定义内容而重新定义。如要改变定义后的数 据属性，需要证明重新定义与原定义的一致性c o h e r e n c e ；如要改变定义内容， 即给出另一种定义形式，则需要证明前后两个定义具有兼容性c o m p a t i b i l i t y 。 2 6miz a r 语言系统中的定理证明 m i z a r 语言系统是基于j a s k o w s k i 自然演绎推理的古典逻辑构建而成的，拥有 符合古典逻辑推理的基本证明方法。 2 6 1 定理证明格式 1 、简单命题 t h e o r e mp p r o o f t h u sp ： e n d ： 2 、与命题( & ) t h e o r e m p 【x 】q 【y 】 p r 0 0 f t h u s “x 】； t h u sq 【y 】； e n d ； 3 、推导命题( i m p l i e s ) t h e o r e m p 【x 】i m p l i e sq 【x 】 ：p 【x 】是关于x 的一个命题 ：q 【x 】是关于y 的一个命题 ：p 【x 】号q 【x 】 p r o o f a s s u m e “x 】； t h u sq 【x 】； e n d ： 4 、等价命题( i 仃) t h e o r e m “x 】i 仃q 【x 】 p r 0 0 f t h u s “x 】i m p l i e sq 【x 】； t h u sp 【x 】i m p l i e sq 【x 】； e n d ： 或者 t h e o r e m p 【x 】i f ! fq 【x 】 p r 0 0 f h e r e b y a s s u m e “x 】； t h u sq 【x 】； e n d ； a s s u m ep 【x 】； t h u sq 【x 】； e n d ： 5 、或命题( o r ) t h e o r e m p 【x 】o rq 【x 】 p r o o f a s s u m en o tp 【x 】； t h u sq 【x 】； e n d ： ：p 【x 】营q 【x 】 ：这个e n d 与h e r e b y 相对应，成对出现。 6 、全称命题( f o r h o m s ) t h e o r e m f l o rx b e i n gs e th o l d sp 【x 】 p r o o f l e txb es e t ； t h u s “x 】； e n d ： 7 、存在命题( e x s t ) t h e o r e me xxb e i n gs e ts tp 【x 】 p r o o f 青岛科技大学研究生学位论文 t a k e x ： t h u sp 【x 】； e n d ： 2 6 2 定理证明方法 1 、直接法 从命题的条件开始，通过合理的推导得出命题结论的方法就叫做直接法。 2 、矛盾法 又称为问接法、反证法，即假设命题结论的否命题成立，通过推导，最终得 出与命题条件矛盾的结论。“c o n t r a d i c t i o n ”的使用是矛盾法的标志。如： a i m p l i e sb p r o o f a s s u m ea ： a s s u m en o tb ： ：假设非b 成立 t h u sc o n t r a d i c t i o n ； ：证明矛盾，说明a 与非b 不能同时成立 e n d ： 3 、分步证明法 分步法是将整个大命题拆分成多个独立的分命题，然后通过对各个分命题的 证明，来完成对整个大命题的证明。 4 、等价命题证明法( 双向法) 等价命题即双向命题，也是互推命题。如命题“pi f f q ”，其中蕴含两个独立 命题“pi m p l i e sq ”和qi m p l i e sp ”。 、5 、 单一否定法( 证明或命题) 单一否定法即否定其中一个命题的结论，通过合理推理，完成另一个命题的 证明方法。 如命题“po rq ”： po rq p r o o f a s s u m en o tp ； t h u sq ； e n d ： p 或p o rq 1 3 一元函数高阶导数在m i z a r 语言系统下的实现研究 p r 0 0 f a s s u m et h a ta ：n o tpa n db ：n o tq ； t h u sc o n t r a d i c t i o n ； ：无理法法证明p 或q e n d ： 2 7miz a r 语言系统的检验及优化命令 m i z a r 语言系统在文章检验及文章内容优化方面的功能是尤为突出的。以下是 文章撰写过程中常用的几个命令： 1 、m i z f 检查推理过程的正确与否。这是在论文写作过程中最常用的一个命令。 如有错误，系统会给出相应的提示，告知错误出现的位置以及错误的类型。然后 我们按照系统的提示进行修改和检测，直至完全j 下确。 2 、l i s t v o c 显示某篇文章的词汇文件。 3 、c h e c k v