Abstract: The numerical verification of geometry theorem proving makes use of numerical computation instead of symbolic computation to improve the efficiency, but there are still problems about the efficiency of complex propositions in practice. This paper attempts the parallel computation method to improve the efficiency, analyzes the partitioning, communication and the task-scheduling algorithm with the MPI programming model, realizes the parallel numerical verification algorithm with MPICH2, and tests the efficiency of algorithm through the parallel performance measure, then the results are satisfied.

Key words: Mechanical geometry theorem proving, Parallel numerical method, Task pool, Parallel performance measure

摘要： 几何定理证明的数值验证法以数值计算代替符号计算来提高效率，但是在实际应用中对复杂命题的解题效率还存在问题。该文尝试用并行计算方法来提高算法效率，分析了MPI编程模型下的任务划分、通信组织、任务调度等问题，并在MPICH2下实现了数值并行验证算法，对算法的并行性能指标进行了测试，得到了较好的结果。

关键词: 几何定理机器证明, 数值并行法, 任务池, 并行性能量度