几何定理机器证明的并行前向推理

几何定理证明的前推法能够产生传统形式的可读证明，在定理机器证明领域占有重要的地位。但是传统算法在实际应用中对复杂命题的解题效率还存在问题。本文尝试用并行计算方法来提高算法效率，分析了前向推理在消息传递编程模型下的任务划分、通信组织、任务调度等问题，并在MPICH 2下实现了并行前向推理算法，实测的并行性能指标表明，对于一些较复杂的命题，此算法能显著减少推理时间。

The Parallel Forward Reasoning for Geometry Theorem Proving

The forward reasoning for geometry theorem proving can produce the traditional readable proving, thus plays a special role in the mechanical theorem proving. As to the traditional algorithm, there are still problems about the efficiency for complex propositions in practice. The authors attempt to use the parallel computation method to improve the efficiency, analyze the partitioning, communication and the task-scheduling algorithm with the message-passing programming model, implement the parallel forward reasoning algorithm with MPICH 2, and then test the efficiency of algorithm through the parallel performance measure.