2.2.8 定理证明器竞赛和著名定理证明器
自动定理证明领域的权威国际会议有 CADE 和 IJCAR，它们均是每两年召开一次，交替召开。美国迈阿密大学的 Geoff Sutcliffe 每年都在 CADE 或 IJCAR 上组织机器定理证明大赛 CASC(CADE ATP System Competition)，主要面向命题逻辑和一阶逻辑证明器。Sutcliffe还维护一个TPTP(Thousands of Problems for Theorem Provers)网站，是 CASC 的比赛题库，也是公认的检验一阶逻辑证明器性能的 benchmark。在 2000 年以前的比赛中，Otter 是多个组别的冠军，2005年后英国曼彻斯特大学的Vampire 后来居上，至今一直维持领先状况。定理证明程序可用于软硬件验证，例如 Vampire 曾被微软公司用来进行软件系统验证。
美国阿贡国家实验室的 William McCune 在上世纪九十年代使用
C 语言实现了Otter 定理证明器，Otter 实现了当时定理证明里最先进
的所有技术，在 CASC 比赛中获得多个组别的冠军。例如，归结原理中的删除策略要求删除被包含的子句，包含测试时定理证明器中最耗时的部分。McCune 最早把项索引引入定理证明器。Otter 主要用到两种项索引，一种是路径索引，另一种是 McCune 提出的差别树索引 (discrimination tree indexing)，这项技术极大地提高了定理证明器的效率[104] 。
McCune 利用 Otter 的模块开发了专门用于等词推理的证明器 EQP。1996 年 10 月，McCune 使用 EQP 证明了罗宾斯猜想[95] 。这是数学家罗宾斯(Herbert Robbins)1933 年提出的一个关于布尔代数的猜想，60 多年来从未被证明。EQP 在一台 486 机器上运行 13 天给出证明，之后又在一台 IBM RS/6000 工作站上运行 7 天进行验证。阿贡国家实验室的定理证明小组在 2006 年被撤销，被认为是符号派低潮的标志性事件。