| Author | Tran Quoc Nam |
| Call Number | AIT Thesis no. CS-92-29 |
| Subject(s) | Geometry, Algebraic
|
| Note | A thesis submitted in partial fulfillment of requirement for the degree of Master of Science, School of Engineering and Technology |
| Publisher | Asian Institute of Technology |
| Abstract | 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. |
| Year | 1992 |
| Type | Thesis |
| School | School of Engineering and Technology (SET) |
| Department | Department of Information and Communications Technologies (DICT) |
| Academic Program/FoS | Computer Science (CS) |
| Chairperson(s) | Kanchana Kanchanasut |
| Examination Committee(s) | Huynh Ngoc Phien ;Hosomura, Tsukasa |
| Scholarship Donor(s) | The Government of Australia. ; |
| Degree | Thesis (M.Sc.) - Asian Institute of Technology, 1992 |