随着对计算机系统安全性、可靠性需求的提高,形式化方法得到了更多的重视。定理证明是重要的形式化技术之一,它用于验证数学定理的正确性。定理证明器可以帮助用户以轻松的、可靠的方式对定理进行证明。本文实现了一个一阶逻辑定理证明器,它使用相继式演算作为交互式定理证明的演绎系统,使用叠加法作为自动定理证明的演绎系统。本文首先对一阶逻辑和序理论进行了论述,为接下来介绍演绎系统做了知识的预备。然后分析介绍了相继式演算、归结原理和叠加法这三种演绎系统。接着本文描述了定理证明器中各个模块的功能及联系,然后分别从交互式定理证明、自动定理证明的角度对每个模块的设计和实现进行了介绍。最后以若干用例演示了证明器的功能并以问题集测试了证明器的能力。通过本文实现的定理证明器,用户可以在图形界面上方便的进行交互式定理证明,也可以调用自动定理证明模块尝试自动解决问题,或者通过两者之间的配合解决问题。未来可以在这基础上支持更多的逻辑,提高描述能力,也可以对自动定理证明能力进行加强。