An Tran Quoc Nam creator Kanchana Kanchanasut Chairperson Huynh, Ngoc Phien Examination Committee Hosomura, Tsukasa Examination Committee The Government of Australia Scolarship Donor text th Bangkok Asian Institute of Technology 1992 monographic eng

print

72 leaves 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 Geometry, Algebraic Asian Institute of Technology. http://203.159.5.9/ait-thesis/detail.php?q=B16657 http://203.159.5.9/ait-thesis/detail.php?q=B16657 050698 20260817162107.0