| The research in mechanical theorem proving has great significance in the theory and the practice. 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.This article combines mechanical geometry theorem proving with the parallel computation, and mainly discusses the parallel algorithm of the forward reasoning and the parallel numerical verification method, then puts it into realization and tests it under the MPICH parallel computation experiment environment. The main tasks of this article are as follows:(1) It is introduced the fundamental theory of mechanical geometry theorem proving and the parallel computation, several kinds of parallel programming models, then constructs the parallel computation experiment environment with MPICH. It is introduced the test of MPI under point-to-point and group communication conditions. It is essential for the following work and the algorithm optimization.(2) Based on the task/channel model, the article analyzes the task partitioning and the communication about forward reasoning, and has presented the program framework for MPI environment. Also it discusses the key problems for improving the efficiency of the forward reasoning. After analysis of the realization of task-scheduling algorithm, the expression about execution time has been presented.(3) Based on the task/channel model, the article analyzes the partitioning and the communication about the parallel numerical verification method, and has presented the program algorithm framework for MPI environment. It carries on the analysis to the dynamic and the static task-scheduling algorithm, and through the time expression comparison, chooses the appropriate task-scheduling algorithm.
|
PDF Full Text Request