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