Institutional Repository
| automated generation of readable proofs for constructive geometry statements with the mass point method | |
| Zou Yu; Zhang Jingzhong | |
| 2011 | |
| Conference Name | 8th International Workshop on Automated Deduction in Geometry, ADG 2010 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 221-258 |
| Conference Date | July 22, 2010 - July 24, 2010 |
| Conference Place | Munich, Germany |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642250699 |
| Department | (1) College of Computer Science and Educational Software Guangzhou University Guangzhou 510006 China; (2) Chengdu Institute for Computer Applications Chinese Academy of Sciences Chengdu 610041 China |
| English Abstract | 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. |
| Keyword | Algorithms Automation |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16302 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Zou Yu,Zhang Jingzhong. automated generation of readable proofs for constructive geometry statements with the mass point method[C],2011:221-258. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment