A REVIEW AND PROSPECT OF READABLE MACHINE PROOFS FOR GEOMETRY THEOREMS

在半世纪研究以后，在几何学证明的机械定理在自动化推理领域里成为了一个活跃研究话题。这评论在为包括搜索方法，没有坐标的方法，和正式逻辑方法的几何学定理产生可读的机器证明自动化上包含三条途径。关于这些途径的一些关键问题也被讨论。而且，作者为几何学定理为可读的机器证明建议三个进一步的研究方向，包括几何学不平等，聪明的几何学软件和机器学习。

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.