定理机器证明的研究已有将近50年的历史,并已经在数理逻辑、初等代数和几何学等学科取得显著成功。关于集合论的定理机器证明研究,有关文献报道用布尔代数的方法可以把集合论的定理证明问题转化为代数问题,但是这类问题的可读证明方法,目前尚未查到有关报道。许多国内外的著名数学软件中,集合论等式型定理的推理方面的功能也比较弱。本论文以人工智能中的搜索算法为基础,研究集合论等式型定理可读证明的机械化方法。 本课题所做的工作包括: 1、通过比较各种搜索算法,选择了盲目搜索算法中渐进最优的迭代加深算法构建推理树,并作了必要的改良,以加速搜索路径的产生。 2、通过研究手工证明和专家经验,总结出几条启发式的规则引导搜索:根据使用频率将公式重新排序;添加了公式反向使用规则;判断左右式长短以决定证明方向;分析结果倒序进栈以保证大的匹配结果优先扩展。 3、利用编程语言Lisp的特点,寻找了一些适合计算机处理的方法,如推理的内部数据用前缀形式。 4、使用了一些方法加速调试,如:先用其他易输入的半角符号代替难输入的全角集合运算符,调通程序;先缩小规模,验证程序的执行过程;运用注解方便测试与修改;如果真实数据过于复杂或难以获得,第一遍采用仿真数据测试,将复杂结果与变量输出到文件监视。 5、采取一些措施,产生详细推理说明。在每一步代换推理前,记录所用的规则以及使用该规则的理由。 6、通过比较数理逻辑和集合论相关的规则,将定理分类推理,基本定理作为经验常识,直接输出结果,不需要说明,加快了证明速度。这一设计可以让宏运算不必都化成基本定理推理,简化证明过程。 本文前三章介绍本课题所涉及的相关的理论以及本文工作构想。第四章引入易于分析和设计修改的PAD图,介绍主程序和处理边界问题的程序。第五章以系统的三个核心程序为例,用可以推广的方式探讨了调试技巧。最后作者指出了本文工作进一步努力的方向:增加搜索策略的灵活性、启发函数和学习功能以及研究规则库和搜索策略的动态调整方法。