在计算机上实现证明计算被称为定理证明。除了针对PL1子集或特殊应用程序的专业证明，现在存在完整谓词逻辑和高阶逻辑的全系列自动化证明，其中只有少数将在此讨论。可以在[McC]中找到最重要系统的概述。
最古老的解决方案之一是在芝加哥阿贡国家实验室开发的。基于1963年开始的早期发展，Otter [Kal01]于1984年创建。最重要的是，Otter成功应用于数学专业领域，可以从其主页学到：
“目前，Otter的主要应用是抽象代数和形式逻辑的研究。Otter及其前身已经被用来回答有限半群，三元布尔代数，逻辑演算，组合逻辑，群论，格理论和代数几何等领域的许多开放性问题。
几年后，慕尼黑科技大学创建了基于快速PROLOG技术的高性能证明器SETHEO [LSBB92]。为了达到更高的性能，并以PARTHEO的名义开发了并行计算机的实现。事实证明，在定理证明中使用特殊硬件是不值得的，因为在AI的其他领域也是如此，因为这些计算机很快被更快的处理器和更智能的算法所取代。慕尼黑也是E
[Sch02]的诞生地，这是一个获奖的现代方程式证明者，我们将在下一个例子中熟悉它。在E的主页上，您可以阅读以下紧凑，具有讽刺意味的特征。
zation，其第二部分偶然适用于今天存在的所有自动化证明者。
“E是句法逻辑的纯粹等式定理证明者。这意味着它是一个程序，你可以将一个数学规范（在具有相等性的条件逻辑中）和一个假设填充到，然后将永远运行，耗尽所有的机器资源。偶尔它会找到假设的证明并告诉你😉。“
找到真正命题的证据显然是如此困难，以至于搜索只是极少，或者只是在很长一段时间后才会成功 – 如果有的话。我们将在Chap中更详细地讨论这个问题。4.应该提到的是，不仅计算机，而且大多数人都难以找到严格的形式证据。
虽然显然计算机本身在许多情况下无法找到证据，但下一个最好的事情是构建半自动工作并允许与用户密切合作的系统。因此，人类可以更好地应用他对特殊应用领域的知识，并可能限制对证据的搜索。高阶谓词逻辑最成功的交互式证明之一是Is- abelle [NPW02]，它是剑桥大学和慕尼黑工业大学的共同产品。
任何寻找高性能证明者的人都应该查看CASC（CADE ATP系统竞赛）[SS06]的当前结果。1
在这里，我们发现2001年至2006年的PL1和条款正常形式类别的获胜者是曼彻斯特的证明者Vampire，它使用解决方案变体和特殊的平等方法。萨尔布吕肯马克斯普朗克研究所的Waldmeister系统多年来在平等证明方面一直处于领先地位。
CASC德国系统的许多重要职位表明，自动化定理证明领域的德国研究小组在今天和过去都发挥着主导作用。
