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

Research and development of automated theorem proving system for set theory

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

Up to the present, there isn＇t related research about automated theorem proving of set theory in domestic and overseas. Though the basic status of set theory in the field of mathematics looks realizing mechanization in this field very important, there isn＇t any evolving year in year out. At present, there isn＇t found any system of producing understandable proof. Through the research of artificial intelligence search arithmetic, the mechanization method of automated theorem proving of equation theorem of set theory is proposed. The system can automated produce understandable proof of set theorem and related explain.