数学机械化是以构造性和算法化的方式来研究数学问题,使这些数学问题的计算、推理或证明可机械化甚至自动化地完成。数学问题的机械化,即要求在运算或证明过程中,每前进一步之后,都有一个确定的、必须选择的下一步,按照一条有规律的、刻板的方式,最后得出结论。数学机械化中一个重要的任务是定理机器证明,即研究如何应用计算机程序来证明数学定理,具体地说,如何通过一套符号体系将人脑的推理证明过程形式化,从而转化为一系列可在计算机上自动实现的推理证明过程。拓扑学是近代发展起来的一个研究连续性现象的数学分支。拓扑学主要研究拓扑空间在拓扑变换下的不变性和不变量,是现代数学研究的理论基础之一。拓扑学不仅在数学的其他分支有着重要作用,而且在其他诸如物理、化学、经济、生物等学科中也发挥着重要的作用。拓扑学机械化能为这些学科的发展提供机械化的理论工具,拓扑学机械化也是数学机械化自身发展的需要。但由于拓扑学的研究对象十分抽象其在计算机系统中的表达非常困难,因而以往的定理机器证明或者数学机械化的研究较少涉及拓扑学这个领域。随着计算机技术的飞速发展,计算机定理证明工具的不断丰富及发展为实现拓扑学的定理机器证明带来了契机,Isabelle就是定理证明工具中的佼佼者。Isabelle使用自然演绎规则进行推理,为定理证明系统的开发提供了一个通用的框架。它既支持数学公式的形式化描述,又为公式的逻辑演算提供了证明工具。Isabelle具有丰富的表达能力、灵活高效的命令集、强大的规则库和灵活且易于扩展的策略库,而且其句法易于扩展,证明过程的可读性强,自动化程度高。一般拓扑学是拓扑学的一个基础分支,为其它的拓扑学分支如代数拓扑、几何拓扑、微分拓扑提供了共同的基础。本论文主要围绕着一般拓扑学机械化展开,主要工作包含以下三个部分：第一、基于Isabelle的一般拓扑学机械化。本文采用高阶逻辑的形式语言来表达一般拓扑学中诸如拓扑空间、开集、闭集、邻域、闭包、连续函数等抽象概念,并将这些抽象概念表示为可计算函数形式,使得这些抽象的数学对象能在Isabelle中以λ-演算的形式实现演绎推理。此外,针对计算机可处理的数学对象,详细研究了证明策略序列的构造方法和技巧,如引入策略、重写策略、分类策略等,并采用逐步求精的方式,实现相关的定理机器证明。论文还实现了一般拓扑学中一些基本定理的机器证明,包括黏结引理、Kuratowski定理、杨忠道定理等涉及复杂集合运算的定理机器证明。第二、在机械化一般拓扑学研究基础上,本文使用Isabelle来表达拓扑动力系统所涉及的基本概念,其中包括群、拓扑群、拓扑迁移群等。并从拓扑迁移群的视角对拓扑动力系统进行研究,并实现了相关定理的机器证明。最后,归纳总结了这些定理的机械化证明方法。第三、形式化定理证明工具的实现。本文基于Isabelle开发了一个自动发现与帮助发现定理的机器证明脚本工具—IsabelleHelper。这一工具本质上是一个定理机器证明的专家系统。它不仅建立了数学定理库和定理证明策略库(或定理证明方法库),而且按照公式间的距离对策略库进行分类和排序,从而极大地缩小了搜索空间,提高了证明效率。IsabelleHelper通过对策略库的搜索、匹配、组合等方法来自动发现定理的机器证明,并为使用者提供不同程度的证明帮助,如完整的定理证明脚本生成、下一步证明的提示等。此外IsabelleHelper通过数学服务总线的方式集成了Isabelle和Maple。由于Isabelle是一个类型系统,侧重于定理验证和推理证明,但对于涉及复杂代数计算的推理较为繁琐；而Maple是一个侧重于符号计算的计算机代数系统,能进行灵活、高效的计算及推理,但由于没有统一的验证机制,可能导致错误或无效的证明。因此本文结合这两大工具的优点,基于开源SOA框架Mule实现了Isabelle和Maple的集成,该集成工具进一步提高了定理证明系统的自动证明能力,扩大了定理证明系统的证明范围。