A REVIEW AND PROSPECT OF READABLE MACHINE PROOFS FOR GEOMETRY THEOREMS

作     者：Jianguo JIANG Jingzhong ZHANG 

作者机构：School of MathematicsLiaoning Normal University Laboratory of Computer Reasoning and Trustworthy ComputionUniversity of Electronic Science and Technology of China Chengdu Institute of Computer ApplicationsChinese Academy of Sciences 

出 版 物：《Journal of Systems Science & Complexity》 (系统科学与复杂性学报（英文版）)

年 卷 期：2012年第25卷第4期

页      面：802-820页

核心收录：

学科分类：07[理学] 0701[理学-数学] 070101[理学-基础数学] 

基　　金：supported by the Funds of the Chinese Academy of Sciences for Key Topics in Innovation Engineering under Grant No.KJCX2-YW-S02 

主　　题：Automated geometry reasoning coordinate-free method formal logic method geometric inequality intelligent geometry software machine learning mechanical theorem proving readable machine proof search method. 

摘      要：After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.