群论问题的形式化及验证研究

发布时间：2017-12-19 19:14

  本文关键词：群论问题的形式化及验证研究　出处：《西南交通大学》2017年硕士论文　论文类型：学位论文

  更多相关文章： 形式化方法 一阶逻辑语言 形式化描述 形式化验证 群论

【摘要】：本文以一种典型的形式化方法——逻辑化方法为研究方向,研究如何应用计算机程序证明数学定理。具体地说,如何通过一套逻辑符号体系将人脑的推理证明过程形式化,从而转化为一系列可在计算机上自动实现的推理证明过程。采用形式语言(逻辑语言)表示数学定理、证明过程是定理证明器的一个重要任务,使得数学定理的表述以及定理证明过程的每个步骤能够被计算机程序验证。我们必须使用严格的语法规则和具有明确语义的形式语言表达数学对象,包括定义、命题和证明。本文主要采用一阶逻辑语言对数学中的群论领域进行形式化研究,并使用定理证明系统Prｏｖer9进行形式化验证,主要取得了如下成果:1、基于形式化方法的两个方面——形式化描述与形式化验证,给出了群论相关知识的形式化过程的基本步骤。2、基于TPTP中群论领域一些已经被形式化的结论,给出了群运算封闭性、恒等元、逆元、结合律、消去律、交换律、恒等元的唯一性、逆元的唯一性、满足一定条件的集合的形式化描述方法。从而完成了群论中一些TPTP中缺少的知识的形式化描述,即阿贝尔群、正规子群、正规化子、中心化子等。然后形式化描述了一些相关的命题及定理,并通过定理证明工具Prｏｖer9验证了其形式化描述的正确性。3、选择了群论中的一个开问题,对其形式化描述并求解,根据本文使用的形式化方法,为此开问题的解决做了推进。
【学位授予单位】：西南交通大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：O152

【参考文献】

中国期刊全文数据库 前6条

1 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

2 王敏;;数理逻辑中的命题符号化的几个值得注意的问题[J];科技信息;2010年09期

3 王静;;离散数学教学中关于命题符号化问题的讨论[J];科技信息(科学教研);2008年25期

4 何锋;;离散数学教学中的命题符号化难点讨论[J];计算机教育;2007年17期

5 周宏斌,黄连生,桑田;基于串空间的安全协议形式化验证模型及算法[J];计算机研究与发展;2003年02期

6 闫安,唐稚松;在 XYZ/ E中实现混成实时系统——蒸气锅炉控制问题的解决(英文)[J];软件学报;2000年06期

中国博士学位论文全文数据库 前3条

1 王建林;基于Isabelle平台的一般拓扑学机械化及自动定理证明研究[D];华东师范大学;2012年

2 沈胜宇;模型检验的反例解释[D];国防科学技术大学;2005年

3 王海霞;运算电路的形式化验证方法研究[D];中国科学院研究生院（计算技术研究所）;2004年

中国硕士学位论文全文数据库 前2条

1 李黎明;代数系统和复数理论的形式化及DS编码器的验证应用[D];首都师范大学;2012年

2 刘素姣;一阶谓词逻辑在人工智能中的应用[D];河南大学;2004年

，

本文编号：1309106