几何定理机器证明三十年  

AUTOMATIC THEOREM PROVING FOR THREE DECADES

作　　者：张景中[1,2,3] 李永彬[4] 

机构地区：[1]电子科技大学与中科院成都计算所自动推理联合实验室,成都610054 [2]中国科学院成都计算机应用研究所,成都610041 [3]广州大学计算机与教育软件学院,广州510006 [4]电子科技大学应用数学学院,成都610054

出　　处：《系统科学与数学》2009年第9期1155-1168,共14页Journal of Systems Science and Mathematical Sciences

基　　金："973"(2004CB318000)项目资助

摘　　要：由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今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.

关 键 词：几何定理机器证明 可读证明 代数方法 面积法 基于数据库的搜索法. 

分 类 号：O18[理学—数学] TP18[理学—基础数学]