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

Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment

作　　者：潘斌[1] 郭红霞[2] 

机构地区：[1]成都理工大学信息管理学院,成都610059 [2]成都大学电子信息工程学院,成都610106

出　　处：《电子科技大学学报》2008年第6期908-912,共5页Journal of University of Electronic Science and Technology of China

基　　金：国家973计划基金资助(CB318003)

摘　　要：将几何定理机器证明和并行计算结合起来考虑,尝试用并行计算方法来提高传统定理证明算法效率,探讨了前推法、数值并行法的并行算法,分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题,并用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.

关 键 词：前向推理 并行算法 数值并行法 性能量度 定理证明 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]