A Automatic Create And Prove System For Geometric Inequations Based On Numeric Computation

The automated prove of geometric theorem is one of the most active branch in automated reasoning and symbolic computation. Methods, including geometric algebraic method, deductive database method and paradigmatic prove method have been widely applied in the geometric theorem prove field. In recent years, with the expansion of computer capability and update of its computing speed, the application of computer in mathematical field was deepened. Another method, namely numerical method for theorem prove was also been expanded vigorously. Many numerical methods such as numerical paradigmatic method, parallel numerical method were presented. All those brought out great progress in theorem automatic prove. Nevertheless, all those methods were aimed at equality theorems and inequality theorem still was the difficult problem in automatic reasoning field.In the 1950's, Tarski published the famous article - A Decision Method for Elementary Algebra and Geometry, which declared that real geometric problem can be resolved theoretically. But this method can not be implemented practically to high complexity and was proved to be inefficient. Later, Collins brought forward the Cylindrical Algebraic Decomposition(CAD) method, which enhance the efficiency and can prove some more difficult geometric inequations. Then, along with Wu method, a method combining Wu method and Langrange multipolar has been presented. But all those methods were not good enough because of the lack of general use and efficiency. In 1998, an automated inequality-proving algorithm was presented by Yang Lu based on a mixed method including a so-called cell-decomposition, the method can prove or disprove proposition in an extensive class of geometric and algebraic inequalities involving radicals. However, this method also depends on real algebra system and symbolic computation software and meanwhile is a little bit complicated. Illumined by existent numerical automated theorem prove method, a method to produce and prove geometric inequation is presented in this thesis. Firstly, according to the user's requirement, we use numerical computation to create some geometric inequations based on paradigmatic method. Then, we induct the interval computation and take it as the compute tool to implement the plotting for function-defined image. By the plotted images, we can prove the geometric inequations. The method has three major advantages: Firstly, this method is based on numerical computation, so the efficiency was enhanced greatly; Secondly, it would avoid losing much necessary information of real numbers by adopting interval computation when the computer storage real numbers; Thirdly, owing to the plotting method, it can deviate from the limit of symbolic computation software and algebraic system and can present a simple result which is more understandable. The method is implemented by a Visual C++ program named "create" which tests the validity and efficient of this method.