Automated Theorem Proving Practice with Null Geometric Algebra

被引：0

作者：

LI Hongbo ^{[1
]}

机构：

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

来源：

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：

暂无

中图分类号：

O187 [代数几何];

学科分类号：

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

共 50 条

[21] Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity
Peng, Xicheng
Zhang, Jingzhong
Chen, Mao
Liu, Sannyuya
[J]. JOURNAL OF AUTOMATED REASONING, 2023, 67 (04)
[22] Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity
Xicheng Peng
Jingzhong Zhang
Mao Chen
Sannyuya Liu
[J]. Journal of Automated Reasoning, 2023, 67
[23] Strategy parallelism in automated theorem proving
Wolf, A
Letz, R
[J]. INTERNATIONAL JOURNAL OF PATTERN RECOGNITION AND ARTIFICIAL INTELLIGENCE, 1999, 13 (02) : 219 - 245
[24] AUTOMATED THEOREM-PROVING METHODS
NOSSUM, R
[J]. BIT, 1985, 25 (01): : 51 - 64
[25] Automated discovering and proving for geometric inequalities
Yang, L
Hou, XR
Xia, BC
[J]. AUTOMATED DEDUCTION IN GEOMETRY, PROCEEDINGS, 1999, 1669 : 30 - 46
[26] Automated theorem proving with disjunctive constraints
Ibens, O
[J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING-CP'99, 1999, 1713 : 484 - 485
[27] Strategy selection for automated theorem proving
Wolf, A
[J]. ARTIFICIAL INTELLIGENCE: METHODOLOGY SYSTEMS AND APPLICATIONS, 1998, 1480 : 452 - 465
[28] A tool for automated theorem proving in Agda
Lindblad, F
Benke, M
[J]. TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 154 - 169
[29] Proof simplification and automated theorem proving
Kinyon, Michael
[J]. PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2019, 377 (2140):
[30] Cancellation Patterns in Automatic Geometric Theorem Proving
Apel, Susanne
Richter-Gebert, Juergen
[J]. AUTOMATED DEDUCTION IN GEOMETRY, 2011, 6877 : 1 - 33

← 1 2 3 4 5 →