automated generation of readable proofs for constructive geometry statements with the mass point method

ISCAS OpenIR

	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
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	221-258
会议日期	July 22, 2010 - July 24, 2010
会议地点	Munich, Germany
收录类别	EI
ISSN	0302-9743
ISBN	9783642250699
部门归属	(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
摘要	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.
关键词	Algorithms Automation
语种	英语
内容类型	会议论文
URI标识	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],2011:221-258.