An algebraic approach to mechanical theorem-proving in geometry - Tran Quoc Nam; Kanchana Kanchanasut; Huynh, Ngoc Phien; Hosomura, Tsukasa; The Government of Australia (Bangkok : Asian Institute of Technology, 1992)
Proving theorems in elementary geometry mechanically has been a dream of people for a long time. Starting by Leibnitz in 17th century. Up to now, it has had a long step on this trend with efforts of Hilbert, Taski, Gelenter, Collin and other researchers. Especially, a new elegant algebraic method for proving a class of geometry theorems was proposed by 'Wu Wen Tsung. This method has been implemented by many researchers. Many non-trivial theorem in elementary geometry which are sometimes difficult to prove by human beings could be proven automatically by Wu's method. In this method, a geometry theorem or statement to be proven is usually stated as a finite set of hypotheses implying a conclusion. A hypothesis is either a polynomial equation expressing a geometric relation or a polynomial inequation (the negation of a polynomial equation) expressing a subsidiary condition such as two points are different or two line segments are not on the same line etc., that rules out degenerate cases. A conclusion is a polynomial equation expressing a geometry relation to be derived. Fundamental to Wu's method is the transformation of a set of geometrical hypothesis expressed as polynomials into a triangular form. And check if the zeros of hypothesis polynomials are zeros of conclusion polynomial or not. Wu defined a characteristic set which is a triangular form with some additional properties to ensure the completeness of his geometric theorem prover. The triangulation algorithms given by Wu are not computationally efficient. Kapur and Mundy proposed a weaker definition of triangular form together with algorithms to compute them which are more efficient than 'vVu's. Kapur et al's algorithm, however, produces a large number of intermediate polynomials. In this thesis, we characterize a class of theorem provable by Kapur et al's algorithm and propose a more efficient algorithm which produces the same result. The proposed algorithm produces complete triangular forms, defined herein, called N- triangular form. By this new algorithm, running time and the number of intermediate polynomials are reduced. An implementation of Kapur et al's and the new algorithm using MATHEMATICA 2.0 was carried out to show some experimental results.
A thesis submitted in partial fulfillment of requirement for the degree of Master of Science, School of Engineering and Technology
Thesis (M.Sc.) - Asian Institute of Technology, 1992
Keywords: Geometry, Algebraic