Dissertation > Mathematical sciences and chemical > Mathematics > Geometry, topology

The Proof Methods of Constructive and Non-constructive Geometric Theorems

Author ShenYing
Tutor HouXiaoRong;WangJinPing
School Ningbo University
Course Basic mathematics
Keywords automated theorem proving numeric computation method constructive problems non-constructive problems eliminating method
Type Master's thesis
Year 2008
Downloads 3
Quotes 0
Download Dissertation

Research on automated theorem-proving is a key branch of AI research. Especially in the field of geometric theorem-proving, our Chinese scientists have made great achievements during the last twenty years. They have brought out many effective methods such as Eliminating method, Wu’s Method, Searching method based on Deductive database, Prove by examples ect. Automated proving systems for geometric theorems, which are designed based on those methods, have not only pushed forward the research in this field, but also given useful revelation for theorem-proving in other fields.Currently, the existing methods are mainly used to realize rigid proof of geometric theorems. However, people often find that if there exists some less rigid proof besides that one. Sometimes people have interest in some geometric relations during the proving but not the proof. So it will be more convenient and efficient to study geometric problems. Furthermore, it can not only prove theorems efficiently, but also thoroughly search out useful messages according to the given order.What more, the performance of existing methods need to be further improved in some aspects, such as how to improve the efficiency, and how to realize automated proving of non-constructive problems, which can’t be constructed step by step directly, ect.According to the problems mentioned above, this article puts forward a new method based on numeric computation, called Dynamic Searching Method of Geometric Theorem. Furthermore, according to the characteristic of non-constructive problems, we develop our method to solve such kind of conjectures. It improves the capability of proving method. As well, we have proved some constructive and non-constructive geometric problems based on Eliminating method, making this field much larger.

Related Dissertations
More Dissertations