Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment

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 results demonstrate that proving time of the program is shorten effectively.