Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 4/2023

01-12-2023

Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity

Authors: Xicheng Peng, Jingzhong Zhang, Mao Chen, Sannyuya Liu

Published in: Journal of Automated Reasoning | Issue 4/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

How to automatically generate short and easy-to-understand proofs for geometric theorems has long been an issue of concern in mathematics education. A novel automated geometric theorem proving method based on complex number identities is proposed in this paper, which acts as a bridge between geometry and algebra. According to the proposed method, the geometric relations in the given proposition are first transformed into a complex number expression, then the complex number identity is generated by the elimination method; finally, the closure property under all four operations of real numbers is employed to prove the proposition. A test on more than 300 geometric problems shows that the proposed method is highly effective, and the corresponding proofs are short, with obvious geometric meaning.
previous article Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation
next article Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Literature
1.
Buchberger, B.: Gröebner bases: an algorithmic method in polynomial ideal theory. In: Multidimensional Systems Theory-Progress, Directions and Open Problems in Multidimensional Systems. Reidel Publishing Company, pp. 184–232 (1985)
2.
Cao, N.B., Li, H.B., Zhang, S.P.: Geometric decomposition and its program implementation based on conformal geometric algebra. Acta Mathematicae Applicatae Sinica 30(5), 891–902 (2007). (in Chinese)MATH
3.
Chang, G.Z.: Complex Number Calculation and Geometry Proof. Shanghai Education Press, Shanghai (1980). (in Chinese)
4.
Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel, Boston (1988)MATH
5.
Chou, S.C., Gao, X.S., Zhang, J.Z.: Mechanical geometry theorem proving by vector calculation. In: Proceedings of the 1993 International Symposium on Symbolic and Algebraic Manipulation, Kiev, ACM Press (1993)
6.
Chou, S.C., Gao, X.S., Zhang, J.Z.: A collection of 110 geometry theorems and their machine proofs based on full-angles. TR-94–4, Department of Computer Science, WSU (1994)
7.
Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)CrossRefMATH
8.
Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants I. Multiple and shortest proof generation. J. Autom. Reason. 17(3), 325–347 (1996)MathSciNetCrossRefMATH
9.
Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated generation of readable proofs with geometric invariants II. Theorem proving with full-angles. J. Autom. Reason. 17(3), 349–370 (1996)MathSciNetCrossRefMATH
10.
Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason. 25(3), 219–246 (2000)MathSciNetCrossRefMATH
11.
Chou, S., Schelter, W.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2, 253–273 (1986)CrossRefMATH
12.
Ge, Q., Zhang, J.Z., Chen, M., Peng, X.C.: Automated geometry readable proving based on vector. Chin. J. Comput. 37(8), 1809–1819 (2014)MathSciNet
13.
Johnson, R.A.: Advanced Euclidean geometry. Houghton Mifflin Company, Boston (1929)
14.
Kapur, D.: Geometry theorem proving using Hilbert’s Nullstellensatz. In: Proceedings of the 1986 Symposium on Symbolic and Algebraic Computation, Waterloo, pp. 202–208 (1986)
15.
Li, H., Xu, R., Zhang, N.: On Miquel’s Five-Circle Theorem. In: Li, H., Olver, P.J., Sommer, G. (eds.) Computer Algebra and Geometric Algebra with Applications. IWMM GIAE 2004 2004. Lecture Notes in Computer Science, vol. 3519. Springer, Berlin (2005)
16.
Li, T., Zhang, J.: Machine proofs in geometry based on complex number method. J. Comput. Res. Dev. 50(9), 1963–1969 (2013)
17.
Peng, X.C.: Vector, Complex Number and Particle. China University of Science and Technology Press, Hefei (2014). (in Chinese)
18.
Peng, X.C., Chen, Q.H., Zhang, J.Z., Chen, M.: Automated discovery of geometric theorems based on vector equations. J. Autom. Reason. 65, 711–726 (2021)MathSciNetCrossRefMATH
19.
Tao, L.I., Zou, Y., Zhang, J.Z., et al.: Improvement of the complex mass point method and its application in automated geometry theorem proving. Chin. J. Comput. 38(08), 1640–1647 (2015)MathSciNet
20.
Titu, A., Dorin, A.: Complex Numbers from A to Z. Birkhäuser, Boston (2005)MATH
21.
22.
Wu, W.T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, New York (1994)CrossRef
23.
Wu, W.T.: Mathematics Mechanization. Science Press, Kluwer (2000)
24.
Yang, L., Xia, B.C.: Automated Proving and Discovering on Inequalities. Science Press, Beijing (2008)
25.
Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. J. Autom. Reason. 45(3), 213–241 (2010)CrossRefMATH
26.
Zhang, J.Z., Peng, X.C.: Solving Geometry Problems with Vector Method. Science Press, Beijing (2010). (in Chinese)
27.
Zhang, J.Z., Peng, X.C.: Point Geometry Problem Solving. East China Normal University Press, Shanghai (2020). (in Chinese)
28.
Zhang, J.Z., Peng, X.C., Chen, M.: Self-evident automated proving based on point geometry from the perspective of Wu’s method identity. J. Syst. Sci. Complexity 32(1), 78–94 (2019)MathSciNetCrossRefMATH
29.
Zou, Y., Peng, X.C., Rao, Y.S.: Identity method of geometric theorem proving based on Wu’s method. Science China Math. 51, 289–300 (2021). (in Chinese)MATH
Metadata
Title
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity
Authors
Xicheng Peng
Jingzhong Zhang
Mao Chen
Sannyuya Liu
Publication date
01-12-2023
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 4/2023
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-023-09688-w

Other articles of this Issue 4/2023

Journal of Automated Reasoning 4/2023 Go to the issue

OriginalPaper

Lower Bounds for QCDCL via Formula Gauge

OriginalPaper

Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation

OriginalPaper

Enabling Floating-Point Arithmetic in the Coq Proof Assistant

OriginalPaper

Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments

OriginalPaper

Finitary Type Theories With and Without Contexts

Research

Combining Stable Infiniteness and (Strong) Politeness

Premium Partner

    Image Credits