A deductive database approach to automated geometry theorem proving and discovering

CSpace

	A deductive database approach to automated geometry theorem proving and discovering
	Chou, SC ; Gao, XS ; Zhang, JZ
	2000-10-01
发表期刊	JOURNAL OF AUTOMATED REASONING
ISSN	0168-7433
卷号	25 期号:3 页码:219-246
摘要	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.
关键词	deductive database automated geometry theorem proving and discovering search strategies redundant deduction Skolemization structured database
语种	英语
WOS研究方向	Computer Science
WOS类目	Computer Science, Artificial Intelligence
WOS记录号	WOS:000087594400002
出版者	KLUWER ACADEMIC PUBL
引用统计
文献类型	期刊论文
条目标识符	http://ir.amss.ac.cn/handle/2S8OKBNM/15392
专题	中国科学院数学与系统科学研究院
作者单位	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.