Self-evident Automated Proving Based on Point Geometry from the Perspective of Wu’s Method Identity
The algebraic methods represented by Wu’s method have made significant breakthroughs in the field of geometric theorem proving. Algebraic proofs usually involve large amounts of calculations, thus making it difficult to understand intuitively. However, if the authors look at Wu’s method from the perspective of identity,Wu’s method can be understood easily and can be used to generate new geometric propositions. To make geometric reasoning simpler, more expressive, and richer in geometric meaning, the authors establish a geometric algebraic system (point geometry built on nearly 20 basic properties/formulas about operations on points) while maintaining the advantages of the coordinate method, vector method, and particle geometry method and avoiding their disadvantages. Geometric relations in the propositions and conclusions of a geometric problem are expressed as identical equations of vector polynomials according to point geometry. Thereafter, a proof method that maintains the essence of Wu’s method is introduced to find the relationships between these equations. A test on more than 400 geometry statements shows that the proposed proof method, which is based on identical equations of vector polynomials, is simple and effective. Furthermore, when solving the original problem, this proof method can also help the authors recognize the relationship between the propositions of the problem and help the authors generate new geometric propositions.
KeywordsGeometry algebra point geometry proof method based on identical equations vector geometry Wu’s method
Unable to display preview. Download preview PDF.
- Wu W T, Mathematics Mechanization, Science Press, Kluwer, 2000.Google Scholar
- Leibniz, Math. Schriften, Berlin 1819, Vol. II: 17 & Vol. V: 133.Google Scholar
- Grassmann, Geometrische Analyse, Nabu Press, Leipzig, 1847.Google Scholar
- Li H B, Hestenes D, and Rockwood A, Generalized Homogeneous Coordinates for Computational Geometry, Ed. by Summer G, Geometric Computing with Clifford Algebras, Springer, Heidelberg, 2001.Google Scholar
- Mo S K, Particle Geometry, Chongqing Press, Chongqing, 1992.Google Scholar
- Wang K and Su Z, Automated geometry theorem proving for human-readable proofs, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015), International Conference on Artificial Intelligence AAAI Press, 2015, 1193–1199.Google Scholar
- Yang L and Xia B C, Automated Proving and Discovering on Inequalities, Science Press, Beijing, 2008.Google Scholar
- Chou S C, Gao X S, and Zhang J Z, Mechanical theorem proving by vector calculation, Proc. of International Symposium on Symbolic and Algebraic Computing, Kelantan, 1993, 284–291.Google Scholar
- Zou Y and Zhang J Z, Automated generation of readable proofs for constructive geometry statements with the mass point method, Proc. of the 8th International Workshop on Automated Deduction in Geometry (ADG 2010), LNAI 6877, Springer-Verlag, Berlin Heidelberg, Germany, 2011, 221–258.CrossRefGoogle Scholar
- Zhang J Z, Outlines for point-geometry, Studies in College Mathematics, 2018, 21(1): 1–8.Google Scholar