mis管理实践论文范文

《mis管理实践论文范文》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、信息管理学院课程论文班级：学号：姓名：专业：指导教师：信息管理学院信息资源管理系二OO年月曰（范文）MPI环境下的定理并行自动推理姓名：学号：［摘要］本文将儿何定理机器证明和并行计算结合起来考虑，尝试用并行计算方法来提高传统定理证明算法效率，探讨了前推法、数值并行法的并行算法，分析了两种定理证明算法在消息传递编程模型下的任务划分、通信组织、任务调度等问题，并用MPICH2实现了这两种并行算法，对算法的并行性能指标进行了测试，测试数据表明，两种并行算法在基于MP1-2的并行计算环境下，能很好地发挥并行计算的优势，有效缩短构造性儿何命题机器证明的时

2、间。关键词：前向推理，并行算法，数值并行法，性能量度，定理证明TheParallelAlgorithmsforMechanicalGeometryTheoremProvingAbstractThepaperconsiderscombiningthemechanicalgeometrytheoremprovingwiththeparallelcomputationmethod,attemptstheparallelcomputationmethodtoimprovetheefficiencyoftraditionaltheoremprovinga

3、lgorithms,discussestheparallelalgorithmsoftheforwardreasoningandthenumericalverificationmethod,analyzesthepartitioning,communicationandthetask-schedulingalgorithmwiththemessage-passingprogrammingmodel,implementsthealgorithmswithMPICH2,andthentestsontheefficiencyofthealgorith

4、mswithparallelperformancemetrics.Theresultshowsthattheparallelalgorithmscouldtakeadvantageofparallelcomputation,andobviouslyreducetheprovingtimeofconstructivegeometrictheorems.Keywords：forwardreasoning;parallelalgorithm;parallelnumericalmethod;performancemetrics;theoremprovi

5、ng1刖吕人工智能与自动推理技术的应用十分广泛，几何定理机器证明是其中一个重要的分支。在实际运用中，对很多复杂度较高的问题，现有的算法在合理的时间内还不能解决。20世纪末以来，国外的一些研究人员己经开始尝试将并行计算技术引入到符号计算当中，以解决一些高复杂度的问题山。本文将几何定理机器证明和并行计算结合起来考虑，主要探讨前推法、数值并行法的并行化算法，并在消息传递接口MPI-2的一个具体实现即MPICH2所构建的并行计算环境下进行实现和测试。2理论背景前推法是一种基于规则的推理方法，类似于人的解题过程。前推法有两个特点：（1）能够产生传统形式的

6、可读证明；（2）无论结论是否能够被推出，都能产生大量有用信息。但是，当前推达到推理不动点仍未推出命题结论，并且不能断定命题不成立，需要用其他方法辅助推理，如添加辅助线、使用反证法等。实际上，可以用代数的方法（吴方法、数值验证法等）对命题的真伪做预先判定。数值验证法的基本思想是：要肯定或否定一条初等几何命题，只要检验若干个数值实例即可。与吴方法等代数方法相比，该方法用数值计算代替符号计算以减少解题难度，是很有特色的一种辅助方法。文献［2・3］介绍了前推法的基本理论，关于数值验证法的具体理论阐述，可参看文献［4-5］o3并行算法设计3.1并行前推法

7、并行前推法程序从文件中读入一个儿何命题，将题设条件写入初始信息库，不断将规则库中的规则应用于信息库，直到无法产生新的几何信息，然后检查信息库中是否有命题结论，若存在，则输11!可读证明到文件中，否则，打印命题证明失败的信息。（1）任务划分。对各子步骤的数据依赖关系作分析，结果如图1所示。图1并行化后的数据依赖图于是，每个操作可以映射为一个原始任务，每个原始任务和2个数据单元（条件信息组+规则）相关联。比较好的数据关联策略是所有计算节点采用同样的规则集，不同的条件信息组进入节点进行匹配，这是条件组层次的并行，其并行粒度小，可扩展性也更好。由于任务

8、的数目在编译时无法确定，各个任务之间不需要通信，完成不同任务所花费的时间也不尽相同，所以任务的映射应该在运行期完成，本文选择Master-Slave模