作　　者： ; ; ; (周咸青）;

机构地区： 中国科学院成都计算机应用研究所

出　　处： 《计算机学报》 1995年第5期380-393,共14页

摘　　要： 用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平凡的几何命题．对其中大多数命题，机器自动生成的证明是简明而易于理解的．本文是对这一领域近三年来取得的进展的综述．包括了在非欧几何可读证明方面的最新成果． Can the geometric theorem proofs which are easily understood by people be automatically produced by a computer? This problem did not take any remarkable advances for several decades until 1992 when a break-through took place. For a large class of Euclidean geometry propositions, there is an efficient decision algorithm and then accordingly a computer program by which more than 500 non-trivial geometry theorems were proven. Amongest the proofs produced automatically by computers, most are brief, easily understood, some even nice. This paper is a survey of advances in automated production of 'readable' proofs duning the past three years. Also included is the similar achievement in non-Enclidean geometry at the most recent.

关 键 词： 可读机器证明 几何定理 计算机

领　　域： [理学] [理学] [自动化与计算机技术] [自动化与计算机技术]