Automated Theorem Proving Practice with Null Geometric Algebra

被引：3

作者：

Li Hongbo ^{[1
]}

机构：

[1] Chinese Acad Sci, Univ Chinese Acad Sci, Acad Math & Syst Sci, Key Lab Math Mechanizat, Beijing 100190, Peoples R China

来源：

JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY | 2019年 / 32卷 / 01期

基金：

中国国家自然科学基金;

关键词：

Automated theorem discovering; automated theorem extending; automated theorem proving; Clifford bracket algebra; null geometric algebra;

D O I：

10.1007/s11424-019-8354-2

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

This paper presents the practice of automated theorem proving in Euclidean geometry with null geometric algebra, a combination of Conformal Geometric Algebra and Grassmann-Cayley algebra. This algebra helps generating extremely short and readable proofs: The proofs generated are mostly one-termed or two-termed. Besides, the theorems are naturally extended from qualitative description to quantitative characterization by removing one or more geometric constraints from the hypotheses.

引用

页码：95 / 123

页数：29

共 30 条

[1]

[Anonymous], 1973, Combinatorics and Renormalisation in Quantum Field Theory

[2]

[Anonymous], 1984, BASIC PRINCIPLES MEC

[3]

[Anonymous], 1988, Mechanical Geometry Theorem Proving

[4]

[Anonymous], 2012, Clifford algebra to geometric calculus: a unified language for mathematics and physics

[5]

[Anonymous], INVARIANT METHODS DI

[6]

Brini A, 2001, ALGEBRAIC COMBINATORICS AND COMPUTER SCIENCE, P151

[7]

Cao N, 2006, THESIS CHINESE ACAD

[8]

[曹源昊 CAO Yuanhao], 2009, [系统科学与数学, Journal of Systems Science and Mathematical Sciences], V29, P1189

[9]

Cecil T.E., 1992, Lie Sphere Geometry: With Applications to Submanifolds

[10]

Chou Shang-Ching, 1994, MACHINE PROOFS GEOME, DOI DOI 10.1142/9789812798152

← 1 2 3 →