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

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

CSpace

	Automated short proof generation for projective geometric theorems with Cayley and bracket algebras - I. Incidence geometry
	Li, HB ; Wu, YH
	2003-11-01
发表期刊	JOURNAL OF SYMBOLIC COMPUTATION
ISSN	0747-7171
卷号	36 期号:5 页码:717-762
摘要	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.
关键词	Cayley algebra bracket algebra automated theorem proving projective incidence geometry
DOI	10.1016/S0747-7171(03)00067-1
语种	英语
WOS研究方向	Computer Science ; Mathematics
WOS类目	Computer Science, Theory & Methods ; Mathematics, Applied
WOS记录号	WOS:000186484500003
出版者	ACADEMIC PRESS LTD ELSEVIER SCIENCE LTD
引用统计
文献类型	期刊论文
条目标识符	http://ir.amss.ac.cn/handle/2S8OKBNM/18966
专题	中国科学院数学与系统科学研究院
通讯作者	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.