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 条

[31] SYMBOLIC ALGEBRA AND THEOREM PROVING FOR FAILURE CRITERIA REDUCTION
Michopoulos, John G.
Iliopoulos, Athanasios
[J]. PROCEEDINGS OF THE ASME INTERNATIONAL DESIGN ENGINEERING TECHNICAL CONFERENCES AND COMPUTERS AND INFORMATION IN ENGINEERING CONFERENCE, 2011, VOL 2, PTS A AND B, 2012, : 201 - 211
[32] Automated reasoning and theorem proving in education - Preface
Kapur, D
[J]. JOURNAL OF AUTOMATED REASONING, 2004, 32 (03) : 185 - 186
[33] Automated theorem proving by test set induction
Bouhoula, A
[J]. JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (01) : 47 - 77
[34] Another look at automated theorem-proving
Koblitz, Neal
[J]. JOURNAL OF MATHEMATICAL CRYPTOLOGY, 2007, 1 (04) : 385 - 403
[35] External Sources of Axioms in Automated Theorem Proving
Suda, Martin
Sutcliffe, Geoff
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
[J]. KI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5803 : 281 - +
[36] Proof Documents for Automated Origami Theorem Proving
Ghourabi, Fadoua
Ida, Tetsuo
Kasem, Asem
[J]. AUTOMATED DEDUCTION IN GEOMETRY, 2011, 6877 : 78 - +
[37] Integration of automated and interactive theorem proving in ILF
Dahn, BI
Gehne, J
Honigmann, T
Wolf, A
[J]. AUTOMATED DEDUCTION - CADE-14, 1997, 1249 : 57 - 60
[38] Recent advances in automated theorem proving on inequalities
Yang L.
[J]. Journal of Computer Science and Technology, 1999, 14 (5) : 434 - 446
[39] An Empirical Assessment of Progress in Automated Theorem Proving
Sutcliffe, Geoff
Suttner, Christian
Kotthoff, Lars
Perrault, C. Raymond
Khalid, Zain
[J]. AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 53 - 74
[40] Automated Theorem Proving in GeoGebra: Current Achievements
Francisco Botana
Markus Hohenwarter
Predrag Janičić
Zoltán Kovács
Ivan Petrović
Tomás Recio
Simon Weitzhofer
[J]. Journal of Automated Reasoning, 2015, 55 : 39 - 59

← 1 2 3 4 5 →