【作者】 闫丽慧；

【导师】 郑骏；

【作者基本信息】 华东师范大学 ， 计算机应用技术， 2007， 硕士

【摘要】 自动定理证明(又叫机器定理证明、机械化定理证明等)是人工智能研究的一个重要分枝,是数学、计算机科学的交叉学科,我国科学家在这一领域的研究走在了世界的前列。不仅提出了多种有效的方法,还成功的开发了一些智能的定理证明系统,其中一些成果已经被成功的应用到几何教育领域。但当前机器证明的理论研究进入低潮,自20世纪末以来,国外研究人员尝试将网络并行计算技术引入到一些关键计算问题中,以求得较高的计算效率,国内这方面的研究也处于起步阶段。近年来,随着Web技术的日益发展和Internet的广泛应用,越来越多的人开始研究借助网络解决数学问题,目前绝大部分研究都是以数学信息平台的建设作为重点,在远程和分布式的环境下实现定理的自动证明的研究并不多见。网格计算是新一代的分布式计算方法,用来表述一种适用于高端科学和工程的分布式计算的体系结构。与传统分布式计算的主要区别在于在没有集中控制机制的情况下,通过对计算资源进行大规模共享,满足应用对高性能计算要求,并且这种对计算资源进行大规模共享是动态的、柔性的、安全的和协作式的,解决了常见的网络并行计算系统面临的操作系统、协议的异构性问题。如果将网格计算的技术应用到几何定理证明的方法中,就可以利用网格提供的超级计算能力,实现高效的协作资源共享,提高定理系统的可重用性、交互性及定理证明的效率。本文的工作是以几何定理证明中的数值方法为基础,尝试将网格计算技术应用于几何定理自动证明,探究一种基于网格计算的几何定理证明的实现方法。在充分分析了网络并行计算理论和实现技术的基础之上,提出了针对数值并行法的网格并行计算虚拟模型。并结合网格环境下数值并行计算实现的难点,采用概率性方法对其加以改进,使得该方法在实现时更加简洁、高效,也为网格计算技术在定理自动证明方面的应用、构建基于网格服务的数学系统方面提供了有益的借鉴。更多还原

【Abstract】 The automatic theorem proving (also is called machine theorem proof, mechanized theorem proof and so on) is an important branch of artificial intelligence research, is interdisciplinary studies field between mathematics and computer science. In particular our Chinese scientists has walked in world front row, Not only proposed many kinds of effective methods, but also successfully developed some intelligence theorem proof system, in which some achievements have already been applied in geometry education domain. Currently, the theoretical research of mechanical theorem proving meets hard times. Since the end of 20 century, the overseas researchers have attempted the parallel computation to solve some key problems of symbolic computation in order to get more computation efficiency. But the similar research is still at the start stage in domestic. At present the major part research is focused on mathematics information platform construction, while only seldom work has been done on how to realize the theorem automatic proof research under long-distance and the distributional environment.The grid computation is a new generation distributed computing method, is used for indicating one kind distributed computing architecture that is suitable for advanced technology and project. Compared with the traditional distributed computing method, the main difference is that the grid computation can satisfy the application request for high performance computation through sharing large-scale computation resources, without the central control mechanism. And this kind of large-scale sharing on computation resources is dynamic, flexible, safe and cooperative, and also has solved the isomerism problem arises in operating system and protocol, which is commonly a critical problem in parallel computing system. If the grid computation technology can be successfully applied into the geometry theorem proof method, we can get highly effective cooperation resources sharing, enhance the reusability, interactive ability of the theorem system and improve theorem proof efficiency, through taking advantage of the super computation ability of the grid. In addition, the achievement on mathematics domain can spread rapidly and integrate into the distant learning platform, and tradition mathematics educational model also changes by this way.In this paper, we attempt applying the grid computation technology in the geometry theorem automatic proof method, bring out a new way that can realize geometry theoremproving under grid circumstances, which is based on numerical method of the geometry theorem proof. Further more, due to the difficulty that parallel numerical method meets under the grid environment, we adopt the probabilistic method to modify and improve the original method, which is easier to realize, and has higher efficiency. The adoption of the new method gives model for the application of grid computation technology to the theorem proving area and furthermore to the construction of grid-based mathematic system.更多还原