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

Parallel Forward Reasoning for Mechanical Proving of Geometry Theorem

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

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

出　　处：《华南理工大学学报（自然科学版）》2008年第4期93-97,共5页Journal of South China University of Technology(Natural Science Edition)

基　　金：国家“973”计划资助项目(CB318003)

摘　　要：为了提高传统前向推理算法在几何定理机器证明中的解题效率,采用并行计算方法来组织推理过程,基于消息传递模型,分析了前向推理并行算法的任务划分、通信组织、任务调度等问题,讨论了算法的时间复杂度,并在MPICH 2构建的并行计算环境下实现了并行前向推理算法.对多个几何定理实例进行的并行性能指标测试表明,该算法并行性好,与传统串行算法相比,在证明复杂的几何命题时,能显著减少推理时间.In order to improve the efficiency of the traditional forward reasoning algorithm for the mechanical proving of geometry theorem, this paper uses the parallel computation method to perform the reasoning, analyzes the task partitioning, communication and task-scheduling based on the message-passing programming model, discusses the time complexity of the parallel algorithm, and implements the parallel forward reasoning algorithm with MPICH 2. Test results of the parallel performance metrics for several geometry theorems show that, as compared with the tradi- tional serial algorithm, the proposed algorithm is of better parallelism performance and greatly saves the reasoning time for complex geometry propositions.

关 键 词：并行算法 定理证明 前向推理 主从模式 性能量度 

分 类 号：TP391.6[自动化与计算机技术—计算机应用技术]