（基础数学专业论文）幂零群p群若干性质的计算机证明.pdf

幂零群p 一群若干性质的计算机证明 摘要 l i l l lll ii ii ii ii i i i iiiii 17 4 0 4 9 1 当前，数学问题计算机证明的研究已成为世界各国积极研究的前沿领 域。随着计算机技术的发展，人们己根据机械化方法创建了各种机器语言 来编写程序，在计算机上给出相应数学问题的机器证明。 本文介绍了数学问题计算机证明的m i z a r 语言系统，应用m i z a r 语言 系统对有限群不同问题给出了相应的证明，主要工作如下： 1 在某种意义下将群的子群与群的同余关系同等看待，在m i z a r 语 言系统下定义了群的子集关于子群的上、下近似，证明了粗糙子集的若干 性质； 2 应用群的正规子群与群的同余关系一一对应关系，在m i z a r 语言系 统下得出群的子群关于正规子群的上、下近似并进一步得到群的粗糙子群 的理论： 3 给出了幂零群m i z a r 语言系统下的定义，证明了幂零群的若干性 质和幂零群的充要条件； 4 给出了若干幂零群的充分条件，指明了幂零群与可解群的关系； 5 给出了p 元素m i z a r 语言系统下的定义，证明了p 一群的等价定义， 讨论了p 群的若干性质； 6 在p 群的基础上给出了p 交换群的定义，证明了p 交换群的若干 性质。 以上结果已经通过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 发表。 关键词： 粗糙子群幂零群p 群p 交换群 n i l p o t e n tg r o u p sp - g r o u p s i nc o m p u t e r a b s t r a c t c u r r e n t l y ，t h em a t h e m a t i c sp r o b l e m so nac o m p u t e rt h a th a sb e c o m e a c t i v e l yr e s e a r c hf r o n t i e r i n t h ew o r l d w i t ht h ed e v e l o p m e n to fc o m p u t e r t e c h n o l o g y ，p e o p l eu n d e rv a r i o u sm e c h a n i z e dm e t h o dt oc r e a t e am a c h i n e l a n g u a g ep r o g r a m ，a n do nt h ec o m p u t e rt ot h em a t hp r o b l e mp r o v i n g t 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 em e t h o do f p r o v e i n ga n d a 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 o c a r r y o u tt h e c 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 m ，w es h o u l dg i v et h em e t h o do fm a t h m a t i c d e d u c t i o na n dc 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 y c o m p u t e r ，p r o v es o m ep r o p e r t i e s o ff i n i t eg r o u p su n d e rt h i ss y s t e r m t h e a u t h o r sm a i nw o r ka sf o l l o w s ： 1 r e v i e w e dt h es u b g r o u po fag r o u pa sc o n g r u e n c er e l a t i o n se q u a l l yi na c e r t a i ns e n s e ，t h ed e f i n i t i o no fs u b s e t so ns u b g r o u p so fag r o u pa p p r o x i m a t i o n a r eg i v e n ，s o m ep r o p e r t i e so fr o u g hs u b s e t sa r ep r o v e d ； 2 n o r m a ls u b g r o u p so fg r o u pa n dc o n g r u e n c er e l a t i o n so n e t o o n e r e l a t i o n s h i p s ，s u b g r o u p so nn o r m a ls u b g r o u p so fg r o u pa p p r o x i m a t i o na n d t h e t h e o r yo fr o u g hs u b g r o u p s a r eg i v e n ； 3 t h ed e f i n i t i o no fn i l p o t e n tg r o u pi sg i v e ni nm i z a r ，s o m ep r o p e r t i e so f n i l p o t e n tg r o u pa r ep r o v e da n dt h en e c e s s a r ya n ds u f f i c i e n tc o n d i t i o n so f n i l p o t e n tg r o u pa r ep r o v e d ； 4 s o m en i l p o t e n ts u f f i c i e n tc o n d i t i o n sa r eg i v e n ，a n dt h er e l a t i o n n i l p o t e n ta n ds o l v a b l eg r o u p si si n d i c a t e d ； 5 t h ed e f i n i t i o no fp e l e m e n ti sg i v e n ，t h ee q u i v a l e n td e f i n i t i o n so f p - g r o u p sa r ep r o v e d a sw e l la ss o m ep r o p e r t i e so fp - g r o u p sa r ed i s c u s s e d ； 6 t h ed e f i n i t i o no fp - c o m m u t a t i v eg r o u p si sg i v e no nt h eb a s i so f p - g r o u p s ，a n ds o m ep r o p e r t i e so fp - c o m m u t a t i v eg r o u p s a r ep r o v e d t h e s er e s u l t sh a v eb e e nv e r i f i e db yt h em i z a r ，a n dr e l e v a n tc o n t e n th a s b e e np u b l i s h e di nf o r m a l i z e dm a t h e m a t i c s k e yw o r d s ：r o u g hs u b g r o u p s n i l p o t e n tg r o u p s p - g r o u p sp c o m m u t a t i v eg r o u p s 青岛科技人学研究生学位论文 目录 摘要”i 英文摘要i i 1 绪论 1 1 数学问题计算机证明的历史及发展现状”1 1 2m i z a r 系统的历史和发展现状1 1 3 课题研究的目的和意义一一3 1 4 课题研究的主要内3 2m i z a r 语言 2 1m i z a r 文章结构一”5 2 2m i z a r 语言系统的基本符号和语法词汇7 2 3m i z a r 语言系统的证明方法一8 2 4m i z a r 语言系统中的定义1 2 3 粗糙子群性质的计算机证明 3 1 预备知识分析”1 5 3 2 群的粗糙子集与粗糙子群性质的计算机证明 3 2 1 群的子集关于子群的上、下近似的m i z a r 定义1 6 3 2 2 群的子集关于子群的上、下近似的性质一”1 8 3 2 3 群的子集关于子群的二重近似2 1 3 2 4 群的子群关于子群的上、下近似的计算机证明”2 4 3 2 5 群的子群关于正规子群的二重近似2 8 3 3 最终实现的m i z a r 形式及成果出处的m i z a r 版本一2 9 4 幂零群性质的计算机证明 4 1 预备知识分析3 1 4 2 幂零群性质的计算机证明 4 2 1 环境部设置一3 2 4 2 2 正文部分3 2 4 3 最终实现的m i z a r 形式及成果出处的m i z a r 版本一4 1 5p 一群性质的计算机证明 5 1 预备知识分析4 3 5 2p - 群与p 交换群性质的计算机证明 5 2 1p - 元素与p - 群性质的计算机证明4 3 5 2 2p 群幂指数的计算机证明4 6 5 2 3p 交换群的计算机证明4 7 5 3 最终实现的m i z a r 形式及成果出处的m i z a r 版本”4 9 总结与展望5 1 参考文献5 2 致谢5 5 攻读学位期间发表的学术论文目录5 6 声明5 7 智能 研究与发展至今已有5 0 余年的历史。1 9 5 9 年，美国洛克菲勒大学著名数理 逻辑学家王浩教授设计了一个程序，仅用9 分钟在计算机证明 了r u s s e l w h i t e h e a d 的巨著数学原理中的3 5 0 余条有关命题逻辑的定 理，王浩这一工作的意义在于宣告了用计算机进行数学定理证明的可能性。 特别是他第一次明确提出了“走向数学机械化 ( t o w a r dm e c h a n i c a lm a t h e m a t i c s ) ”。1 9 7 6 年，美国年轻的数学家哈肯 ( h a k e n ) 和阿佩尔( a p p l e ) 在高速电子计算机上耗费12 0 0 小时的计算时间， 证明了困扰了数学家们1 0 0 多年来的“四色定理”。1 9 8 5 年，吴文俊发表了 关于代数方程组的零点，这标志着“吴方法”的诞生，为数学机械化研 究揭开了新的一幕。 1 迄今为止，已有2 9 0 余种 2 机器语言系统可以用来进行数学定理证 明。如a u t o m a t h 3 1 、e l f 、h o l 、l e g o 、t h e o r e m a 4 1 、m i z a r 5 、i m p s 、 a l f 和n u p r l 6 ，7 等系统。尽管它们的初衷不同，却有一个共同的特点： 使用机器语言书写、计算、推理和证明文本性质的数学问题，并使用机器 验证其正确性。其中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 r y ) ，同时在自动智能方面独立开发出强大的“人 机对话功能，引起世界各国的关注 8 ，9 。 1 2miz a r 语言系统的历史和发展现状 m i z a r 语言系统是一种计算机语言系统，是一个专门用来构建m i z a r l 数学知识库的自动推理校验系统。目前，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 版本，在互联网上可随时查阅 1 0 。 m i z a r 语言系统是1 9 7 3 年1 1 月由波兰华沙大学a n d r z e jt r y b u l e c 教 授在华沙大学图书馆学和科学信息学院的一次研讨会上，第一次完整地提 出的，并对这种语言在其功能上的一些必需的特点作了说b 韭j 1 1 ： l 、具有可存储性和可编译性，即撰写的文章可存储于计算机中，可将其全 部或部分内容自动翻译成自然语言； 2 、格式整齐匀称，内容简洁易懂： 3 、具有支撑整个数学领域自动化信息系统的基本要素； 4 、具有查验错误、查证参考文献、删减重复定理的功能； 5 、可实现自动排版功能。 197 4 年，由a n d r z e j t 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 i z a r 语言系统的初级版本m i z a 卜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 ) 。 随后，研究人员对m i z a r - p c 进行了大量的语法和句法改进并最终实 现了其在不同操作系统下的成功运行。 1 0 到目前为止，m i z a r 语言系统已经升级到7 1 1 0 5 版本，m i z a r 数据库 ( m m l ) 中已收录1 0 9 0 多篇文章，2 万多个数学概念，4 5 万多条定理。并 且已经形成了系统化的数学知识领域，这些数学知识几乎涵盖了数学的每 一个分支，如数学分析学、代数学、几何学、图论、数论、范畴理论等领 域。特别是在对连续格的证明及b r o u w e r 不动点、j o r d a n 曲线等定理的证明 中，解决了一些人们用手无法计算和证明的复杂问题，从而显示了m i z a r 语言系统的优越性。同时，它在自动化控制、声音和图像识别等研究领域 也有着广泛的应用。 1 3 课题研究的目的和意义 2 青岛科技大学研究生学位论文 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 的翻译机制，增强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 z a r 语言 系统下证明及解决奠定了理论和实践基础。 1 4 课题研究的主要内容 群论的发展已有1 0 0 多年了，在庞大m i z a r 数据库m m l 中对于群论 的研究只涉及到初步的基础知识，缺少进一步的探讨。在m i z a r 语言系统 下，本文的主要内容如下： 1 在某种意义下将群的子群与群的同余关系同等看待，在m i z a r 语 言系统下定义了群的子集关于子群的上、下近似，证明了粗糙子集的若干 性质； 2 应用群的正规子群与群的同余关系一一对应关系，在m i z a r 语言 系统下得出群的子群关于正规子群的上、下近似并进一步得到群的粗糙子 群的理论； 3 给出了幂零群m i z a r 语言系统下的定义，证明了幂零群的若干性 质和幂零群的充要条件； 4 给出了若干幂零群的充分条件，指明了幂零群与可解群的关系； 5 给出了p 一元素m i z a r 语言系统下的定义，证明了p 一群的等价定义， 讨论了p 一群的若干性质； 6 在p 一群的基础上给出了p 一交换群的定义，证明了p 一交换群的若 干性质。 3 4 青岛科技大学研究生学位论文 2 1m i z a r 文章结构 2m 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 文章包括两部分一一环境部( t h e e n v i r o n m e n ts e c t i o n ) 和正文部分( t h em a i ns e c t i o n ) 。环境部以“e n v i r o n ” 开始，以“： 结束。正文部分以“b e g i n ”开始，以“： 结束，还可根 据需要用“b e g i n 将正文部分分成若干个小部分，如表2 - 1 1 2 ： e n v i r o n t h ee n v i r o n m e n ts e c l ：i o n ( 环境部) b e g i n ：them a i ns e c t i o n ( 正文部分) 表2 1m i z a r 文章的一般结构 t a b 2 1t h ef r a m eo fm i z a ra r t i c l e s 环境部主要说明文章中所引用的词汇、符号、初定义、定理和结构的 出处，如表2 2 。在m i z a r 文章中所使用的系统中已存在的定义或定理，必 须将该定义或定理的出处分别添加到环境部的相应部分中。“v o c a b u l a r y 是文章引用的词汇列表。如果在文章中定义了新的概念、符号或结构等， 同样需要将该文章的缩写名写入环境部中v o c a b u l a r y 部分。缩写名可由自己 命名，以便于在m i z a r 语言系统中的使用和检验。“s i g n a t u r e 是文章所使 用的符号列表，“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 是文章所使用的结构列表。 5 v o c a b u l a r y ( 词汇) q ，口2 ，口 ： s i g n a t u r e ( 符号) j j l ，5 2 ，k ： d e f i n i t i o n s ( 定义) 4 ，畋，丸： t h e o r e m s ( 定理) e l , 乞，： s c h e m e s ( 结构) 正，厶，厶； 表2 2 环境部结构 t a b 2 2t h ee n v i r o n m e n ts e e t i o n 其中a i , b i ，c j ，嗄，乞正表示被引用的文章名。 正文部分是由句子( s e n t e n c e ) 构成，主要包含定义( d e f i n i t i o n ) 和定 理( t h e o r e m ) 。通过定义概念、编写证明、列举特例完成定理的证明，从 而实现理论体系的m i z a r 转化，使理论在m i z a r 语言系统中继续发展。 正文部分中定理证明有固定的格式，即以“p r o o f 开头，以“e n d ： 结束，二者成对出现。对于证明过程中出现的小命题的证明也采取同样的 证明格式，如表2 3 ： t a b 2 3t h ef r a m eo ft h ed e m o n s t r a t i o n 6 青岛科技人学研究生学位论文 2 2m i z a r 语言系统的基本符号和语法词汇 2 2 1m i z a r 语言系统的基本符号 m i z a r 语言的符号是基于纯粹的数学符号和一般的a s c i i 字符相结合的 原则来定义和编写的。主要符号如表2 - 4 1 3 ： 普通数学 命题中的 3v = q ) a s s u m e q ； t h u s p ； ( q = p ) e n d ； 2 3 2 一般命题的m i z a r 表述及证明格式和方法 m i z a r 语言系统下对一般命题的表述和传统数学命题陈述相类似，主要 有一下几种表述方式： 1 简单命题 t h e o r e m p( p 是一个命题) p r o o f t h u sp ； e n d ； 2 与命题( ) 该类命题的证明多采用拆分证明法。如： t h e o r e m p q p r o o f t h u sp ； t h u sq ； e n d ； 3 推导命题( i m p l i e s ) 该类命题的证明多采用直接证明法。如： t h e o r e m pi m p l i e sq p r o o f a s s u m ep ； t h u sq ； h e n c et h e s i s ； 1 0 青岛科技人学研究生学位论文 e n d ； 4 或命题( o r )该类命题的证明多采用单一否定法来实现证明，即 通过否定其中一个命题，完成肯定另一个命题的证明，从而实现整个命题 的方法。或命题的m i z a r 表示形式和证明步骤如下： t h e o r e m p o rq p r o o f a s s u m en o tp ； t h u sq ； e n d ； 5 等价命题( i f f ) 即pi f f q 型命题。该类命题常采用等价证明方法予 以证明。如： t h e o r e m pi f fq( p 营q ) p r o o f t h u spi m p l i e sq ；( 证明pjq ) t h u sq i m p l i e sp ；( 证明qjp ) e n d ； 6 全称命题( f o r h o l d s ) 该类命题证明在m i z a f 中证明格式如下： t h e o r e mf o rxh o l d sp p r o o f l e tx ： t h u sp ： e n d ： 7 存在命题( e x s t 。) 对于这类命题一般用“t a k e ”做总结证明。如： t h e o r e me xxb es e ts tp p r o o f t a k ex ； t h u sp ； e n d ； 事实上，命题在m i z a r 语言系统下表述往往是以上几种基本命题的综 合，如命题pi m p l i e sq li f fq 2 是第三类和第五类的综合，命题e xyb es e ts t p q 是第二类和第七类的综合，因此，定理的证明也是多种证明方法的 综合。 2 4miz a r 语言系统中的定义 m i z a r 语言系统中，对于定义有着严格的分类要求，主要分为谓词定义 ( p r e d i c a t e s ) 、模式定义( m o d e s ) 、算子定义( f i l c t o r s ) 、属性定义( a t t r i b u t e s ) 、 c l u s t e r 定义、结构定义( s t r u c t u r e s ) ，并且对于不同类型的定义，需要从存在 性和惟一性两方面给出逻辑证明，如表2 5 所示【1 4 - ( “”表示需要证明， 无“，表示无需证明。) e x i s t e n c e u n i q u e n e s s m o d e ( 模式) p r e d ( 谓词) f u n c t o r ( 算子) a t t r ( 属性) c l u s t e r 表2 5 定义证明分类 t a b 2 5t h ed e f m i t i o no ft h a tc a t e g o r y 而且这些定义要收录在m m l 的论文中的词汇数据库( v o c 文件) 中。每篇 文章都有一个与之同名的词汇文件( 即v o c 文件) 用来记录新的定义，且以 v o c 为后缀，并与文章本身相关联。不同类型的定义，在词汇文件中的表示 方法不同，具体表示见表2 6 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 表字母)( 定义类型) mm o d e ( 模式) of u n c t o r ( 算子) rp r e d i c a t e ( 谓词) kl e f tf u n c t o rb r a c k e t ( 左括号) l r i g h tf u n c t o rb r a c k e t ( 右括号) gs t r u c t u r e ( 结构) us e l e c t o r ( 函子) va t t r i b u t e ( 属性) 表2 6 定义类型的代表字母表 t a b 2 - 6r e p r e s e n t a t i v eo ft h ea l p h a b e t - d e f i n e dt y p e v o c 文件的创建规则及顺序为：首先填写表示类型的一个大写字母，紧 接新定义的词汇名，其间不可添加空格或任何字符。对于新定义的算子， 在类型字母0 后加新定义词汇名，还可添加空格和1 至u 2 5 5 之间的一个数字， 其中数字表示运算优先级，缺省表示6 4 。如m i z a r 文章h i d d e n 的词汇文件 - h i d d e n v o c 的仓, j 建形式如表2 - 7 【1 6 】： h i d d e n v o c m a n y m r e a l m n a t k 【： l ：】 o + 3 2 o r 表2 7h i d d e n v o c 的创建形式 t a b 2 7h i d d e n v o c 1 4 青岛科技大学研究生学位论文 3 粗糙子群性质的计算机证明 1 9 8 2 年由波兰科学家z p a w l a k 仓a j 立提出的粗糙集理论不但是一 种新型的处理模糊和不确定知识的数学工具，而且是一个不完备信息 的新颖、有效的软计算方法。目前已在人工智能、数据挖掘、模式识 别、决策分析、故障检测等方面得到了广泛的应用粗糙集理论作为一 种数据分析处理理论， 1 7 当前粗糙集理论与代数相结合也是数学 研究中的一个前沿课题。在m m l 数据库中，缺少相应代数结构的m i z a r 表示，在某种意义上将一个群的子群和一个群的同余关系做一一对应，从而 得出群的子集关于子群的上、下近似，群的上、下粗糙子群以及对群的粗 糙子群的二次近似，并完成了相关内容的在m i z a r 语言系统下的证明，收录于 m m l 的文章中，发表于2 0 0 9 年的f o r m a l i z e dm a t h e m a t i c s 期刊。 3 1 预备知识分析 定义3 1 1 1 8 设n 是群g 的一个子群，a 是群g 一个非空子集。则集 合n a = x glx * n a ) ，n a = x gj x * nna a 分别称为集合a 关于群g 的一个子群n 的下、上近似。 定理3 1 1 1 8 - 2 5 对任意的x g ，a ，b 是g 的非空子集，n ，h 是g 的 子群有以下性质： ( 1 ) 若x n a ，贝l j x * n a ； ( 2 ) 若x * n a ，则x n a ； ( 3 ) 若x n a ，则x * nna a ： ( 4 ) 若x * nna o ，则x n a ； ( 5 ) n acacn a ： ( 7 ) n ( anb ) =( n a ) r l ( n b ) ； ( 8 ) n ( au b ) = ( n a ) u ( n b ) ： ( 9 ) 若a c _ b ，贝l jn a c _ n b 且n a n b ； ( 1 0 ) 若n h ，贝0h a n a 且n “a h a ； ( 11 ) ( n 、a ) u ( n b ) 互n ( a ub ) ； ( 1 2 ) ( n 、a ) ( n b ) c n ( a * b ) ； ( 1 3 ) ( n “a ) ( n “b ) ：n ( a * b ) 。 定理3 1 2 2 6 对任意的x g ，a ，b 是g 的非空子集，n ，h 是g 的子群 其二重近似有以下性质： ( 1 ) 若x n 、( n a ) ， n x 幸n n a ； ( 2 ) 若x n 一( n a ) ，则x 幸nn n 、( n 。a ) 囝； ( 3 ) 若x n 一( n a ) ，则x 宰nn ( n a ) a ； ( 4 ) n 、( n 、a ) = n 、a ： ( 5 ) n ( n a ) = n a ： ( 6 ) 若a c n ( n a ) ，贝i jn a n n ( n a ) 定义3 1 2 1 8 群g 的一个非空子集a 称为g 的一个n 、粗糙 正规 子群， 如果a 的一个下近似n a m 群的g 一个 正规 子群。 群g 的一个非空子集a 称为g 的一个n 粗糙 正规 子群，如果a 的一个上 近似n a 是群g 的一个 正规 子群。 定理3 1 3 18 2 5 若n 是群g 的一个正规子群，a 是g 的一个子群，并且 n a ，贝0 ( 1 ) n a 为g 的一个n 、粗糙子群； ( 2 ) n a 为g 的一个n 粗糙子群。 定理3 1 4 1 8 2 5 若设n ，a 是群g 的一个正规子群，且nc a ，则 ( 1 ) n a 为g 的一个n 粗糙正规子群； ( 2 ) n a 为g 的一个n “粗糙正规子群。 3 2 群的粗糙子集与粗糙子群性质的计算机证明 3 2 1 群的子集关于子群的上、下近似的m i z a r 定义 在m i z a r 中给出群的子集关于子群的上、下近似的定义是极其重要的。 算子在m i z a r 中定义有两种形式： 一、直接定义新算子，即定义一个新的函数。由陈述性语言定义的新 算子在m i z a r 中必须证明其存在性和唯一性，否则校验定义不合理，“f u n c ” 和“m e f l l l s ”是它的标志。 二、利用已有的算子模式定义新算子。这种模式定义的新算子在m i z a r 中只需证明正确性或一致性，标志词是“e q u a l s ”。 1 6 青岛科技大学研究生学位论文 在m i z a r 中我们采用第二种算子定义模式来定义群的子集关于子群的 下近似“n 、a ，和群的子集关于子群的上近似“n a ”，其表述与正确性逻 辑证明如下： definition(王) 1 e tgb eg r o u p ，a b es u b s e to f g ； l e tn b es u b g r o u po f g ； f u n cn 、a 一 s u b s e to fg e q u a l s 【xw h e r ex i se l e m e n to fg ：x 事n c = a ； c o r r e c t n e s 一s p r o o f xw h e r ex i se l e m e n to fg ：x 幸nc - - a c - - t h ec a r r i e ro fg p r o o f l e tyb es e t ； a s s u m ey i n xw h e r ex i se l e m e n to fg ：x 幸nc - a ) ； t h e ne xx b e i n ge l e m e n to fg s ty = x & x 幸nc = a ： h e n c et h e s i s ； e n d ； h e n c et h e s i s ； e n d ； f u n cn a s u b s e to fg e q u a l s xw h e r exi se l e m e n t o fg ：x 宰nm e e t sa ； c o r r e c t n e s s p r o o f xw h e r e xi se l e m e n to fg ：x 幸nm e e t sa ) c - - t h ec a r r i e ro fg p r o o f l e tyb es e t ； a s s u m eyi n xw h e r exi se l e m e n to fg ：x nm e e t sa ) ； t h e ne xx b e i n ge l e m e n to fgs ty = x x 木nm e e t sa ； h e n c et h e s i s ； e n d ； h e n c et h e s i s ； e n d ； 1 7 e n d ( 盈_ i 处的e n d 与处的d e f i n i t i o n 对应，两者成对出现。 3 2 2 群的子集关于子群的上、下近似的性质 借助群的子集关于子群的上、下近似的定义在m i z a r 语言系统中讨论群 的子集关于子群的上、下近似的性质，其具体表述如下： t h e o r e m g r o u p 一1 1 ：1 2 f o rx b e i n ge l e m e n to fg s txi nn 、ah o l d sx 宰nc - - a ； t h e o r e m ：g r o u p 一1 1 ：1 3 f o rx b e i n ge l e m e n to fg s tx 书nc - ah o l d sxi nn 、a ； t h e o r e m g r o u p 一1 1 ：1 4 f o rx b e i n ge l e m e n to fg s txi nn ah o l d sx 幸nm e e t sa ； t h e o r e m g r o u p 一1 1 ：1 5 f o rx b e i n ge l e m e n to fg s tx 宰nm e e t sah o l d sxi nn a ； t h e o r e m g r o u p