集合论等式型定理机器证明系统的研究与开发

摘要

集合论定理机器证明,至今在国内外尚无相关研究.虽然集合论在数学领域中所处的基础地位显得在这一领域实现机械化极其重要,但是多年来尚无进展.到目前为止,还没有发现能产生可读证明的系统.通过对人工智能搜索算法的研究,提出了集合论等式型定理证明的机械化方法.实现的系统能自动生成定理的可读证明以及相关的说明.