Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry

doi:10.1016/S0747-7171(03)00067-1

	Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry
	Li, HB ; Wu, YH
刊名	JOURNAL OF SYMBOLIC COMPUTATION
	2003-11-01
卷号	36 期号:5 页码:717-762
关键词	Cayley algebra bracket algebra automated theorem proving projective incidence geometry
ISSN号	0747-7171
DOI	10.1016/S0747-7171(03)00067-1
英文摘要	In this paper we establish the Cayley expansion theory on factored and shortest expansions of typical Cayley expressions in two- and three-dimensional projective geometry. We set up a group of Cayley factorization formulae based on the classification of Cayley expansions. We continue to establish three powerful simplification techniques in bracket computation. On top of the Cayley expansions and simplifications, together with a set of elimination rules, we design an algorithm that can produce extremely short proofs in two- and three-dimensional projective geometry. The techniques developed here can be immediately applied to other symbolic computation tasks involving brackets. (C) 2003 Elsevier Ltd. All rights reserved.
WOS研究方向	Computer Science ; Mathematics
语种	英语
出版者	ACADEMIC PRESS LTD ELSEVIER SCIENCE LTD
WOS记录号	WOS:000186484500003
内容类型	期刊论文
源URL	[http://ir.amss.ac.cn/handle/2S8OKBNM/18965]
专题	中国科学院数学与系统科学研究院
通讯作者	Li, HB
作者单位	1.Chinese Acad Sci, Acad Math & Syst Sci, Math Mech Key Lab, Beijing 100080, Peoples R China 2.Chinese Acad Sci, Inst Automat, Natl Lab Pattern Recognit, Beijing 100080, Peoples R China
推荐引用方式 GB/T 7714	Li, HB,Wu, YH. Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry[J]. JOURNAL OF SYMBOLIC COMPUTATION,2003,36(5):717-762.
APA	Li, HB,&Wu, YH.(2003).Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry.JOURNAL OF SYMBOLIC COMPUTATION,36(5),717-762.
MLA	Li, HB,et al."Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry".JOURNAL OF SYMBOLIC COMPUTATION 36.5(2003):717-762.