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

华南理工大学学报（自然科学版） ›› 2008, Vol. 36 ›› Issue (4): 93-97.

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

潘斌¹郭红霞²

1. 成都理工大学信息管理学院, 四川成都 610059； 2. 成都大学电子信息工程学院, 四川成都 610106

收稿日期:2007-03-14 修回日期:2007-06-05 出版日期:2008-04-25 发布日期:2008-04-25
通信作者: 潘斌（1978-），男，博士，主要从事MIS、并行工程、专家系统方面的研究． E-mail:pan_swpi2003@163．com
作者简介:潘斌（1978-），男，博士，主要从事MIS、并行工程、专家系统方面的研究．
基金资助:
国家“973”计划资助项目（CB318003）

Parallel Forward Reasoning for Mechanical Proving of Geometry Theorem

Pan Bin¹ Guo Hong-xia²

1. College of Information Management, Chengdu University of Technology, Chengdu 610059, Sichuan, China; 2. College of Electronic and Information Engineering, Chengdu University, Chengdu 610106, Sichuan, China

Received:2007-03-14 Revised:2007-06-05 Online:2008-04-25 Published:2008-04-25
Contact: 潘斌（1978-），男，博士，主要从事MIS、并行工程、专家系统方面的研究． E-mail:pan_swpi2003@163．com
About author:潘斌（1978-），男，博士，主要从事MIS、并行工程、专家系统方面的研究．
Supported by:
国家“973”计划资助项目（CB318003）

摘要/Abstract

摘要： 为了提高传统前向推理算法在几何定理机器证明中的解题效率,采用并行计算方法来组织推理过程,基于消息传递模型,分析了前向推理并行算法的任务划分、通信组织、任务调度等问题,讨论了算法的时间复杂度,并在MPICH 2构建的并行计算环境下实现了并行前向推理算法.对多个几何定理实例进行的并行性能指标测试表明,该算法并行性好,与传统串行算法相比,在证明复杂的几何命题时,能显著减少推理时间.

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

Abstract:

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.

Key words: parallel algorithm, theorem proving, forward reasoning, master-slave model, performance metric

潘斌郭红霞 . 几何定理机器证明的并行前向推理[J]. 华南理工大学学报（自然科学版）, 2008, 36(4): 93-97.

Pan Bin Guo Hong-xia. Parallel Forward Reasoning for Mechanical Proving of Geometry Theorem[J]. Journal of South China University of Technology (Natural Science Edition), 2008, 36(4): 93-97.

[1]	徐华张庭. 云计算环境下基于改进离散粒子群的并行调度算法[J]. 华南理工大学学报（自然科学版）, 2015, 43(9): 95-99.
[2]	刘勇奚建清黄东平贾连印苗德成. 图形处理器上CSB⁺- 树索引的并行构建算法[J]. 华南理工大学学报（自然科学版）, 2014, 42(1): 123-127,134.
[3]	郭黎利刘明夺姜晓斐. 沃尔什序列组的两个新性质及其推论[J]. 华南理工大学学报（自然科学版）, 2013, 41(6): 35-41.
[4]	奚建清游进国汤德佑肖伟吉. 基于MapReduce的封闭立方体并行计算方法[J]. 华南理工大学学报（自然科学版）, 2009, 37(1): 91-95,112.
[5]	齐德昱李小薪. 命题公式的一种演绎判定方法[J]. 华南理工大学学报（自然科学版）, 2008, 36(9): 71-76.
[6]	魏关锋钱宇姚平经. 多流股换热器网络综合问题的优化算法设计[J]. 华南理工大学学报（自然科学版）, 2006, 34(8): 6-12.