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