MPI环境下的几何定理并行自动推理

Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment

将几何定理机器证明和并行计算结合起来考虑,尝试用并行计算方法来提高传统定理证明算法效率,探讨了前推法、数值并行法的并行算法,分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题,并用MPICH2实现了这两种并行算法,对算法的并行性能指标进行了测试,测试数据表明,两种并行算法在基于MPI-2的并行计算环境下,能很好地发挥并行计算的优势,有效缩短构造性几何命题机器证明的时间。

This paper describes two parallel algorithms for geometry theorem proving based on the two traditional methods： the forward reasoning and the numerical verification method. The task partitioning, communication, and the task-scheduling algorithm are also described with the message-passing programming model. Tests on the parallel computing environment are reported. The esults demonstrate that proving time of the program is shorten effectively.