Automated Theorem Proving Practice with Null Geometric Algebra

被引：0

作者：

Hongbo Li

机构：

[1] Chinese Academy of Sciences,Key Laboratory of Mathematics Mechanization, Academy of Mathematics and Systems Science, University of Chinese Academy of Sciences

来源：

Journal of Systems Science and Complexity | 2019年 / 32卷

关键词：

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

D O I：

暂无

中图分类号：

学科分类号：

摘要：

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

页数：28

共 50 条

[1] Automated Theorem Proving Practice with Null Geometric Algebra
LI Hongbo
[J]. Journal of Systems Science & Complexity, 2019, 32 (01) : 95 - 123
[2] Automated Theorem Proving Practice with Null Geometric Algebra
Li Hongbo
[J]. JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY, 2019, 32 (01) : 95 - 123
[3] Automated geometric theorem proving, Clifford bracket algebra and Clifford expansions
Li, HB
[J]. ADVANCES IN ANALYSIS AND GEOMETRY: NEW DEVELOPMENTS USING CLIFFORD ALGEBRAS, 2004, : 345 - 363
[4] Automated Geometric Theorem Proving: Wu's Method
Elias, Joran
[J]. MATHEMATICS ENTHUSIAST, 2006, 3 (01): : 3 - 50
[5] Projective geometric theorem proving with Grassmann-Cayley algebra
Li, Hongbo
[J]. HERMANN GRASSMANN: FROM PAST TO FUTURE: GRASSMANN'S WORK IN CONTEXT, 2011, : 275 - 285
[6] Automated theorem proving in the homogeneous model with Clifford bracket algebra
Li, HB
[J]. APPLICATIONS OF GEOMETRIC ALGEBRA IN COMPUTER SCIENCE AND ENGINEERING, 2002, : 69 - 78
[7] Automated Geometric Reasoning with Geometric Algebra: Theory and Practice
Li, Hongbo
[J]. PROCEEDINGS OF THE 2017 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC'17), 2017, : 7 - 8
[8] Algebraic representation, elimination and expansion in automated geometric theorem proving
Li, HB
[J]. AUTOMATED DEDUCTION IN GEOMETRY, 2004, 2930 : 106 - 123
[9] Automated theorem proving
Li, HB
[J]. GEOMETRIC ALGEBRA WITH APPLICATIONS IN SCIENCE AND ENGINEERING, 2001, : 110 - +
[10] Automated theorem proving
Plaisted, David A.
[J]. WILEY INTERDISCIPLINARY REVIEWS-COGNITIVE SCIENCE, 2014, 5 (02) : 115 - 128

← 1 2 3 4 5 →