形式方法中的定理证明器综述
A Survey on Theorem Provers in Formal Methods
摘要：
机械推理是处于数理逻辑和人工智能交叉点的一个关键研究领域。开发机械推理系统（也称为定理证明器）的主要目的是使数学家能够通过计算机程序证明定理。然而，这些工具随着时间的推移而发展，现在在复杂和大规模系统的建模和推理中发挥着至关重要的作用，特别是安全关键系统。从技术上讲，数学形式主义和自动推理为基础的方法来执行推理，并在定理证明生成证明。在文献中，有一个全面的文件，可以提供适当的指导，定理证明器的设计，性能，逻辑框架，优势，差异和应用领域的偏好的短缺。在这项工作中，40多个定理证明器进行了详细的研究和比较，提出了一个全面的分析和评价这些工具。定理证明器的各种参数的基础上，其中包括：实现架构，使用的逻辑和演算，库支持，自动化水平，编程范式，程序设计语言，差异和应用领域进行了调查。
英文摘要：
Mechanical reasoning is a key area of research that lies at the crossroads of mathematical logic and artificial intelligence. The main aim to develop mechanical reasoning systems (also known as theorem provers) was to enable mathematicians to prove theorems by computer programs. However, these tools evolved with time and now play vital role in the modeling and reasoning about complex and large-scale systems, especially safety-critical systems. Technically, mathematical formalisms and automated reasoning based-approaches are employed to perform inferences and to generate proofs in theorem provers. In literature, there is a shortage of comprehensive documents that can provide proper guidance about the preferences of theorem provers with respect to their designs, performances, logical frameworks, strengths, differences and their application areas. In this work, more than 40 theorem provers are studied in detail and compared to present a comprehensive analysis and evaluation of these tools. Theorem provers are investigated based on various parameters, which includes: implementation architecture, logic and calculus used, library support, level of automation, programming paradigm, programming language, differences and application areas.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
