几何定理机器证明三十年

AUTOMATIC THEOREM PROVING FOR THREE DECADES

由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索法更能生成其可读的证明.几何不等式机器证明的研究,由于多项式完全判别系统的建立,也有了突破.研究领域已由机器证明扩展为包括几何作图在内的一般几何问题的机器求解,并有了实际的应用.

Originating the traditional, meaning and interesting Euclid＇s geometry, theorem proving in geometry plays an increasingly important role in the research of automated reasoning. Since the pioneering work of Wu, automated geometry theorem proving has been an active area of research for three decades. Extensive and detailed studies have produced automatic proofs, which even can be readable, for a large number of classic and more recent geometric theorems and geometric inequalities. They have even supported the discovering of new theorems. Several main methods for automated geometry theorem proving are chiefly introduced in the survey.