定理机器证明是人工智能的一个重要研究领域，被应用在数学定理证明、协议验证、软件和硬件的形式化验证等方面。提高定理机器证明的效率仍然受到人工智能界的重视。人们开发了各种定理证明系统，主要有自动化和交互式两种类型。Isabelle/Isay/HOL(以下简称Isabelle)是基于高阶逻辑的交互式定理证明器，它是由英国剑桥大学的Lawrence C.Paulson教授和德国慕尼黑技术大学的Tobias Nipkow教授于1986年开始联合开发的，并在不断的更新和发展。在Isabelle中定理证明的主要方法是策略，证明过程是由用户提交策略，再由机器执行策略的交互过程。本文在分析了Isabelle最基本的证明策略的基础上，通过在Isabelle集成环境中添加控制模块(Ctrl Block)，完成了一种并行自动化证明策略的系统设计。该控制模块负责解释并执行并行策略，完成各进程间的通信。该系统的运行环境为支持MPI编程标准的并行计算机或微机机群，由多个协同完成证明任务的Isabelle进程组成，采用主从模式的大粒度并行算法。主进程位于用户计算机中，从进程位于选定的机群中。主进程负责控制整个并行程序，分配证明任务给从进程，等待从进程报告证明的结果，再根据结果判断证明是完成还是失败。从进程等待主进程给它分配证明任务，接到并完成任务后向主进程报告证明的结果，然后继续等待主进程分配的任务或停止指令。