Research On Automatic Theorem Proving Based On Grid Computation

The automatic theorem proving (also is called machine theorem proof, mechanized theorem proof and so on) is an important branch of artificial intelligence research, is interdisciplinary studies field between mathematics and computer science. In particular our Chinese scientists has walked in world front row, Not only proposed many kinds of effective methods, but also successfully developed some intelligence theorem proof system, in which some achievements have already been applied in geometry education domain. Currently, the theoretical research of mechanical theorem proving meets hard times. Since the end of 20 century, the overseas researchers have attempted the parallel computation to solve some key problems of symbolic computation in order to get more computation efficiency. But the similar research is still at the start stage in domestic. At present the major part research is focused on mathematics information platform construction, while only seldom work has been done on how to realize the theorem automatic proof research under long-distance and the distributional environment.The grid computation is a new generation distributed computing method, is used for indicating one kind distributed computing architecture that is suitable for advanced technology and project. Compared with the traditional distributed computing method, the main difference is that the grid computation can satisfy the application request for high performance computation through sharing large-scale computation resources, without the central control mechanism. And this kind of large-scale sharing on computation resources is dynamic, flexible, safe and cooperative, and also has solved the isomerism problem arises in operating system and protocol, which is commonly a critical problem in parallel computing system. If the grid computation technology can be successfully applied into the geometry theorem proof method, we can get highly effective cooperation resources sharing, enhance the reusability, interactive ability of the theorem system and improve theorem proof efficiency, through taking advantage of the super computation ability of the grid. In addition, the achievement on mathematics domain can spread rapidly and integrate into the distant learning platform, and tradition mathematics educational model also changes by this way.In this paper, we attempt applying the grid computation technology in the geometry theorem automatic proof method, bring out a new way that can realize geometry theoremproving under grid circumstances, which is based on numerical method of the geometry theorem proof. Further more, due to the difficulty that parallel numerical method meets under the grid environment, we adopt the probabilistic method to modify and improve the original method, which is easier to realize, and has higher efficiency. The adoption of the new method gives model for the application of grid computation technology to the theorem proving area and furthermore to the construction of grid-based mathematic system.