The algebraic methods represented by Wu's method have made signi?cant breakthroughs in the ?eld of geometric theorem proving. Algebraic proofs usually involve large amounts of calculations, thus making it diffcult...The algebraic methods represented by Wu's method have made signi?cant breakthroughs in the ?eld of geometric theorem proving. Algebraic proofs usually involve large amounts of calculations, thus making it diffcult 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 ?nd 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 e?ective. 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.展开更多
An automated reasoning method, based on Wu’s method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used ...An automated reasoning method, based on Wu’s method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used to simplify one of Chern’s theorems: "The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces." Some other theorems are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks.展开更多
基金supported in part by the National Key Research and Development Program of China under Grant No.2017YFB1401302the National Natural Science Foundation of China under Grant No.41671377
文摘The algebraic methods represented by Wu's method have made signi?cant breakthroughs in the ?eld of geometric theorem proving. Algebraic proofs usually involve large amounts of calculations, thus making it diffcult 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 ?nd 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 e?ective. 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.
基金Project supported partially by the National Natural Science Foundation of China.
文摘An automated reasoning method, based on Wu’s method and calculus of differential forms, is proposed for mechanical theorem proving in local theory of space surfaces in differential geometry. The method has been used to simplify one of Chern’s theorems: "The non-trivial families of isometric surfaces having the same principal curvatures are W-surfaces." Some other theorems are also tested by this method. The proofs are generally simpler than those in differential geometry textbooks.
