04138nam a2200409 0 4500 20260817162107.0 050698 th eng .b10065969 AIT Thesis no. CS-92-29 Tran Quoc Nam An algebraic approach to mechanical theorem-proving in geometry Bangkok : Asian Institute of Technology, 1992 72 leaves Thesis ; no. CS-92-29 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 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. Geometry, Algebraic Kanchana Kanchanasut, Chairperson Huynh, Ngoc Phien, Examination Committee Hosomura, Tsukasa, Examination Committee The Government of Australia., Scolarship Donor Asian Institute of Technology. Thesis ; no. CS-92-29 Full-Text http://203.159.5.9/ait-thesis/detail.php?q=B16657 .b10065969 mnait u 240409 2 951012 m a u 3 mnait mnait mnarc 20 40 Barcode : 30050003100921 CREATED : 1994-05-16 RECORD # : i10062890 LPATRON : 0 LCHKIN : - # RENEWALS : 0 # OVERDUE : 0 IUSE3 : 0 TOT CHKOUT : 0 TOT RENEW : 0 Barcode : 30050003100939 CREATED : 1994-05-16 RECORD # : i10062907 LPATRON : 0 LCHKIN : - # RENEWALS : 0 # OVERDUE : 0 IUSE3 : 0 TOT CHKOUT : 0 TOT RENEW : 0 Barcode : 30050120357230 CREATED : 2016-10-06 RECORD # : i13032677 LPATRON : 0 LCHKIN : - # RENEWALS : 0 # OVERDUE : 0 IUSE3 : 0 TOT CHKOUT : 0 TOT RENEW : 0 3836 3836 0 0 0 0 MAIN MAIN mnait 2026-08-17 10.00 0 AIT Thesis no. CS-92-29 30050003100921 2026-08-17 16:21:07 1 2026-08-17 20 0 0 0 0 MAIN MAIN mnait 2026-08-17 10.00 0 AIT Thesis no. CS-92-29 30050003100939 2026-08-17 16:21:07 2 2026-08-17 20 0 0 0 0 MAIN MAIN mnarc 2026-08-17 0 AIT Thesis no. CS-92-29 30050120357230 2026-08-17 16:21:07 2026-08-17 40