自动推理

自动推理（）是计算机科学和数理逻辑的一个交叉领域，致力于理解推理的不同方面。自动推理的研究有助于开发能够让计算机完全或近乎完全自动地进行推理的计算机程序。虽然自动推理被视为人工智能的一个子领域，但它也与理论计算机科学和哲学有密切联系。

自动推理中发展最成熟的子领域包括自动定理证明（以及交互式定理证明）和。在类比推理、归纳推理和溯因推理方面也有大量研究工作。其他重要主题包括不确定性推理和非单调逻辑推理。自动推理的工具和技术包括经典逻辑和演算、模糊逻辑、贝叶斯推断、最大熵推理以及许多非形式化的特设技术。以及利用符号化的来防止幻觉的架构。

早期历史
形式逻辑的发展在自动推理领域中发挥了重要作用，而自动推理本身又推动了人工智能的发展。形式证明是一种每个逻辑推论都已回溯到数学基本公理的证明，所有中间逻辑步骤无一例外地得到提供，无需诉诸直觉。

一些人认为1957年在康奈尔大学召开的暑期会议——汇聚了众多逻辑学家和计算机科学家——是自动推理（或者说自动演绎）的起源。另一些人则认为，其起源更早，可以追溯到1955年纽厄尔、肖和西蒙的逻辑理论家程序，或者马丁·戴维斯1954年对普雷斯伯格算术判定程序的实现。

自动推理虽然是一个重要且热门的研究领域，但在1980年代和1990年代初经历了“人工智慧低谷”。此后该领域得以复兴。例如，2005年微软开始在多个内部项目中使用验证技术，并计划在2012版的Visual C中纳入逻辑规约和检查语言。

逻辑理论家（LT）是1956年由艾伦·纽厄尔、克利夫·肖和赫伯特·西蒙开发的第一个旨在“模拟人类推理”的定理证明程序。它在《数学原理》第二章的52条定理中证明了38条，其中一条定理的证明比怀特海和罗素的原证明更简洁。

以下是一些具有里程碑意义的自动证明示例：

证明系统
NQTHM（Boyer–Moore定理证明器）的设计受到约翰·麦卡锡和伍迪·布莱索的影响。该项目于1971年在苏格兰爱丁堡启动，是一个用Pure Lisp构建的全自动定理证明器，其特点包括使用Lisp作为工作逻辑、依赖全递归函数的定义原则、广泛使用重写和“符号求值”，以及基于符号求值失败的归纳启发式。

HOL Light以OCaml编写，旨在拥有简洁清晰的逻辑基础和精简的实现，是一个用于经典高阶逻辑的证明助手。

Rocq（原名Coq）是在法国开发的自动证明助手，能够从规约中自动提取可执行的OCaml或Haskell程序。属性、程序和证明使用同一种称为归纳构造演算（CIC）的语言进行形式化。

应用
自动推理最常被用于构建自动定理证明器。然而，定理证明器通常需要一定的人工引导才能有效运行，因此更一般地被称为证明助手。在某些情况下，这些证明器提出了证明定理的新方法。自动推理程序被应用于解决形式逻辑、数学和计算机科学、逻辑编程、软件和硬件验证、电路设计等领域中日益增多的问题。TPTP问题库（Sutcliffe和Suttner, 1998）定期更新，自动演绎会议（CADE）定期举办自动定理证明竞赛，其题目选自TPTP库。

参见

• 自动机器学习（AutoML）
• 自动定理证明
• （IJCAR）
• （Journal of Automated Reasoning）
• （AAR）

参考文献