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

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

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

潘斌, 郭红霞

文章导航 > 电子科技大学学报 > 2008 > 37(6): 908-912

潘斌, 郭红霞. MPI环境下的几何定理并行自动推理[J]. 电子科技大学学报, 2008, 37(6): 908-912.

引用本文:

潘斌, 郭红霞. MPI环境下的几何定理并行自动推理[J]. 电子科技大学学报, 2008, 37(6): 908-912.

PAN Bin, GUO Hong-xia. Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment[J]. Journal of University of Electronic Science and Technology of China, 2008, 37(6): 908-912.

Citation:

PAN Bin, GUO Hong-xia. Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment[J]. Journal of University of Electronic Science and Technology of China, 2008, 37(6): 908-912.

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

潘斌¹,
郭红霞²

1.
成都理工大学信息管理学院成都 610059;
2.
成都大学电子信息工程学院成都 610106

基金项目:

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

作者简介:
潘斌(1978-),男,博士生,主要从事MIS、并行工程、专家系统方面的研究.

中图分类号: TP311

Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment

PAN Bin¹,
GUO Hong-xia²

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

摘要: 将几何定理机器证明和并行计算结合起来考虑,尝试用并行计算方法来提高传统定理证明算法效率,探讨了前推法、数值并行法的并行算法,分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题,并用MPICH2实现了这两种并行算法,对算法的并行性能指标进行了测试,测试数据表明,两种并行算法在基于MPI-2的并行计算环境下,能很好地发挥并行计算的优势,有效缩短构造性几何命题机器证明的时间。
- 前向推理 /
- 并行算法 /
- 数值并行法 /
- 性能量度 /
- 定理证明
Abstract: 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.
- forward reasoning /
- parallel algorithm /
- parallel numerical method /
- performance metrics /
- theorem proving

[1]	杨峰, 周飞, 潘丽丽, 林静然. 基于交错方向乘子法的并行GPS信号捕获算法 . 电子科技大学学报, 2020, 49(2): 187-193. doi: 10.12178/1001-0548.2018112
[2]	卞琛, 于炯, 修位蓉, 廖彬, 英昌甜, 鲁亮. Spark框架并行度推断算法 . 电子科技大学学报, 2019, 48(4): 567-574. doi: 10.3969/j.issn.1001-0548.2019.04.014
[3]	范天龙, 朱燕燕, 吴蕾蕾, 任晓龙, 吕琳媛. DHC定理在有向含权网络上的推广及应用 . 电子科技大学学报, 2017, 46(5): 766-776. doi: 10.3969/j.issn.1001-0548.2017.05.020
[4]	梁瑞仕, 姜云飞, 杨会志. 基于有序爬山法的前向启发式搜索规划 . 电子科技大学学报, 2013, 42(3): 464-469. doi: 10.3969/j.issn.1001-0548.2013.03.028
[5]	李建江, 张磊, 李兴钢, 陈翔, 黄义双. CUDA架构下的灰度图像匹配并行算法 . 电子科技大学学报, 2012, 41(1): 110-113. doi: 10.3969/j.issn.1001-0548.2012.01.021
[6]	钟秀琴, 符红光, 丁盘苹. 基于本体与Prolog的平面几何定理证明 . 电子科技大学学报, 2011, 40(3): 429-434. doi: 10.3969/j.issn.1001-0548.2011.03.020
[7]	陈晖, 易克初, 李文铎. 高速数字解调中的并行处理算法 . 电子科技大学学报, 2010, 39(3): 340-345. doi: 10.3969/j.issn.1001-0548.2010.03.003
[8]	赖生建, 王秉中, 黄廷祝. 共享内存系统中高效并行FDTD计算方案 . 电子科技大学学报, 2010, 39(5): 680-683. doi: 10.3969/j.issn.1001-0548.2010.05.007
[9]	王鹏, 常征. 算法隐含并行性的物理模型 . 电子科技大学学报, 2009, 38(4): 588-591. doi: 10.3969/j.issn.1001-0548.2009.04.026
[10]	于泠, 陈波. 入侵数据特征并行选择算法 . 电子科技大学学报, 2008, 37(2): 266-269.
[11]	廖臣, 祝大军, 刘盛纲. 五点差分格式求解泊松方程并行算法的研究 . 电子科技大学学报, 2008, 37(1): 81-83,127.
[12]	杨浩淼, 孙世新, 李洪伟. 前向安全的基于身份加密方案 . 电子科技大学学报, 2007, 36(3): 534-537.
[13]	曹建蜀, 汪学刚. 机载前向阵雷达近程杂波频移补偿 . 电子科技大学学报, 2006, 35(3): 320-323.
[14]	唐续, 刘心松, 杨峰, 刘谐. 分布式并行服务器中的高性能通信研究 . 电子科技大学学报, 2005, 34(2): 213-216.
[15]	郑洪, 肖先赐. MUSIC算法在高速并行处理机上的实现 . 电子科技大学学报, 2005, 34(6): 759-762.
[16]	戴波, 刘辉, 郑方伟, 郑婵. 二维到达角和极化参数的并行化设计 . 电子科技大学学报, 2004, 33(2): 125-128.
[17]	孙世新, 陈平安, 张艳. 与FFT并行算法相适应的体系结构探讨 . 电子科技大学学报, 2000, 29(5): 535-539.
[18]	范勇, 王兆明, 黄香馥. 快速并行σ_i预测CORDIC算法 . 电子科技大学学报, 1998, 27(1): 29-32.
[19]	林水生, 黄顺吉. 一种合成孔径雷达成像处理的并行算法 . 电子科技大学学报, 1998, 27(1): 1-4.
[20]	林水生, 黄顺吉. 一种面向MIMD并行机实现的FFT并行算法 . 电子科技大学学报, 1997, 26(6): 621-626.

WeChat

点击查看大图

计量

文章访问数: 3586
HTML全文浏览量: 169
PDF下载量: 46
被引次数: 0

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

潘斌¹,
郭红霞²

1. 成都理工大学信息管理学院成都 610059;

2. 成都大学电子信息工程学院成都 610106

基金项目:

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

作者简介:
潘斌(1978-),男,博士生,主要从事MIS、并行工程、专家系统方面的研究.

收稿日期: 2007-04-08
修回日期: 2008-01-24
刊出日期: 2008-12-15

中图分类号: TP311

关键词:

摘要: 将几何定理机器证明和并行计算结合起来考虑,尝试用并行计算方法来提高传统定理证明算法效率,探讨了前推法、数值并行法的并行算法,分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题,并用MPICH2实现了这两种并行算法,对算法的并行性能指标进行了测试,测试数据表明,两种并行算法在基于MPI-2的并行计算环境下,能很好地发挥并行计算的优势,有效缩短构造性几何命题机器证明的时间。

English Abstract

潘斌, 郭红霞. MPI环境下的几何定理并行自动推理[J]. 电子科技大学学报, 2008, 37(6): 908-912.

引用本文:

潘斌, 郭红霞. MPI环境下的几何定理并行自动推理[J]. 电子科技大学学报, 2008, 37(6): 908-912.

PAN Bin, GUO Hong-xia. Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment[J]. Journal of University of Electronic Science and Technology of China, 2008, 37(6): 908-912.

Citation:

PAN Bin, GUO Hong-xia. Parallel Automated Reasoning for Geometry Theorem Proving Based on MPI Environment[J]. Journal of University of Electronic Science and Technology of China, 2008, 37(6): 908-912.

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

版权所有 © 《电子科技大学学报》编辑部

地址: 成都市建设北路二段四号电子科技大学主楼中350室电话: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

本系统由北京仁和汇智信息技术有限公司开发