A deductive database approach to automated geometry theorem proving and discovering
文献类型：期刊论文
| 作者 | Chou, SC; Gao, XS; Zhang, JZ |
| 刊名 | JOURNAL OF AUTOMATED REASONING
 |
| 出版日期 | 2000-10-01 |
| 卷号 | 25期号:3页码:219-246 |
| 关键词 | deductive database automated geometry theorem proving and discovering search strategies redundant deduction Skolemization structured database |
| ISSN号 | 0168-7433 |
| 英文摘要 | We report our effort to build a geometry deductive database, which can be used to find the fixpoint for a geometric configuration. The system can find all the properties of the configuration that can be deduced using a fixed set of geometric rules. To control the size of the database, we propose the idea of a structured deductive database. Our experiments show that this technique could reduce the size of the database by one hundred times. We propose the data-based search strategy to improve the efficiency of forward chaining. We also make clear progress in the problems of how to select good geometric rules, how to add auxiliary points, and how to construct numerical diagrams as models automatically. The program is tested with 160 nontrivial geometry configurations. For these geometric configurations, the program not only finds most of their well-known properties but also often gives unexpected results, some of which are possibly new. Also, the proofs generated by the program are generally short and totally geometric. |
| WOS研究方向 | Computer Science |
| 语种 | 英语 |
| WOS记录号 | WOS:000087594400002 |
| 出版者 | KLUWER ACADEMIC PUBL |
| 源URL | [http://ir.amss.ac.cn/handle/2S8OKBNM/15391]  |
| 专题 | 中国科学院数学与系统科学研究院 |
| 作者单位 | 1.Wichita State Univ, Dept Comp Sci, Wichita, KS 67260 USA 2.Acad Sinica, Inst Syst Sci, Beijing 100080, Peoples R China 3.Acad Sinica, Inst Comp App, Chengdu 610015, Peoples R China |
| 推荐引用方式 GB/T 7714 | Chou, SC,Gao, XS,Zhang, JZ. A deductive database approach to automated geometry theorem proving and discovering[J]. JOURNAL OF AUTOMATED REASONING,2000,25(3):219-246. |
| APA | Chou, SC,Gao, XS,&Zhang, JZ.(2000).A deductive database approach to automated geometry theorem proving and discovering.JOURNAL OF AUTOMATED REASONING,25(3),219-246. |
| MLA | Chou, SC,et al."A deductive database approach to automated geometry theorem proving and discovering".JOURNAL OF AUTOMATED REASONING 25.3(2000):219-246. |
入库方式： OAI收割
来源：数学与系统科学研究院
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。