机器定理证明在数学定理证明、协议验证、软件和硬件的形式化验证等方面发挥出越来越重要的作用。为了提高定理证明器的工作效率和自动化程度,人们开发了各种定理证明系统,主要有自动化和交互式两种类型。 Isabelle是一种用来构造交互式定理证明器的逻辑框架,由它构造的Isabelle/HOL是一种功能完备的定理证明系统。在Isabelle中证明定理的主要方法是策略,即完成一步或多步基本推理的程序。证明的过程是用户选择策略,然后机器执行策略,如此反复直到完成证明。所以,在Isabelle中定理证明的核心问题就是找到能够完成证明的一个策略序列。 本文设计并实现了一种以Isabelle为基础的并行定理证明环境,它通过在多个运行Isabelle的服务器上同时执行各自的策略来实现对定理的并行证明。然后以此为基础讨论几种并行证明策略及一种自动化证明策略。该自动化证明策略的基本思想是对给定的策略集,系统以并行方式同时尝试由其中的策略组成的各策略序列,从而实现自动定理证明的目的。