Journal of South China University of Technology (Natural Science Edition) ›› 2008, Vol. 36 ›› Issue (4): 93-97.

• Computer Science & Technology • Previous Articles     Next Articles

Parallel Forward Reasoning for Mechanical Proving of Geometry Theorem

Pan Bin1  Guo Hong-xia2   

  1.  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:

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