| 几何定理机器证明三十年 |
| |
| 引用本文： | 张景中,李永彬.几何定理机器证明三十年[J].系统科学与数学,2009,29(9):1155-1168. |
| |
| 作者姓名： | 张景中 李永彬 |
| |
| 作者单位： | 1. 电子科技大学与中科院成都计算所自动推理联合实验室,成都,610054;中国科学院成都计算机应用研究所,成都,610041,广州大学计算机与教育软件学院,广州,510006
2. 电子科技大学应用数学学院,成都,610054 |
| |
| 基金项目： | 国家重点基础研究发展规划(973计划) |
| |
| 摘 要： | 由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索法更能生成其可读的证明.几何不等式机器证明的研究,由于多项式完全判别系统的建立,也有了突破.研究领域已由机器证明扩展为包括几何作图在内的一般几何问题的机器求解,并有了实际的应用.
|
| 关 键 词： | 几何定理机器证明 可读证明 代数方法 面积法 基于数据库的搜索法. |
| 收稿时间： | 2009-6-26 |
AUTOMATIC THEOREM PROVING FOR THREE DECADES |
| |
| ZHANG Jingzhong,LI Yongbin.AUTOMATIC THEOREM PROVING FOR THREE DECADES[J].Journal of Systems Science and Mathematical Sciences,2009,29(9):1155-1168. |
| |
| Authors: | ZHANG Jingzhong LI Yongbin |
| |
| Institution: | (1)UESTC-CICACAS Joint Laboratory of Automated Reasoning, University of Electronic Science and Technology of China, Chengdu 610054;Chengdu Institude of Computer Applications, Chinese Academy of Sciences, Chendu 610041; Institute for Educational Software, Guangzhou University, Guangzhou510006;(2)School of Applied Mathematic, University of Electronic Science and Technology of China, Chengdu 610054. |
| |
| Abstract: | 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. |
| |
| Keywords: | Automated geometry theorem proving Wu-characteristic set algebraic methods readable proof area method deductive database method |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《系统科学与数学》浏览原始摘要信息 |
| 点击此处可从《系统科学与数学》下载免费的PDF全文 |
|
