automated generation of readable proofs for constructive geometry statements with the mass point method
文献类型：会议论文
| 作者 | Zou Yu ; Zhang Jingzhong |
| 出版日期 | 2011 |
| 会议名称 | 8th International Workshop on Automated Deduction in Geometry, ADG 2010 |
| 会议日期 | July 22, 2010 - July 24, 2010 |
| 会议地点 | Munich, Germany |
| 关键词 | Algorithms Automation |
| 页码 | 221-258 |
| 中文摘要 | The existing readable machine proving methods deal with geometry problems using some geometric quantities. In this paper, we focus on the mass point method which directly deals with the geometric points rather than the geometric quantities. We propose two algorithms, Mass Point Method and Complex Mass Point Method, which can deal with the Hilbert intersection point statements in affine geometry and the linear constructive geometry statements in metric geometry respectively. The two algorithms are implemented in Maple as provers. The results of hundreds of non-trivial geometry statements run by our provers show that the mass point method is efficient and the machine proofs are human-readable. © 2011 Springer-Verlag. |
| 英文摘要 | The existing readable machine proving methods deal with geometry problems using some geometric quantities. In this paper, we focus on the mass point method which directly deals with the geometric points rather than the geometric quantities. We propose two algorithms, Mass Point Method and Complex Mass Point Method, which can deal with the Hilbert intersection point statements in affine geometry and the linear constructive geometry statements in metric geometry respectively. The two algorithms are implemented in Maple as provers. The results of hundreds of non-trivial geometry statements run by our provers show that the mass point method is efficient and the machine proofs are human-readable. © 2011 Springer-Verlag. |
| 收录类别 | EI |
| 会议录 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| 语种 | 英语 |
| ISSN号 | 0302-9743 |
| ISBN号 | 9783642250699 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16302]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Zou Yu,Zhang Jingzhong. automated generation of readable proofs for constructive geometry statements with the mass point method[C]. 见:8th International Workshop on Automated Deduction in Geometry, ADG 2010. Munich, Germany. July 22, 2010 - July 24, 2010. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。