计算机逻辑

计算机逻辑是逻辑领域和计算机科学领域之间的重叠部分。 该主题基本上可以分为三个主要领域：理论基础和分析；使用计算机技术来帮助逻辑学家；将逻辑概念用于计算机应用等。

逻辑在计算机科学中起着基础性的作用。 一些特别重要的逻辑关键领域是可计算性理论（以前称为递归理论）、模态逻辑和范畴论。 计算理论基于逻辑学家和数学家定义的概念，例如 Alonzo Church 和 Alan Turing。 Church 首先使用他的 lambda 可定义性概念证明了算法无法解决的问题的存在。 图灵首次对所谓的机械过程进行了令人信服的分析，库尔特·哥德尔断言他发现图灵的分析是完美的。此外，逻辑和计算机科学之间理论重叠的其他一些主要领域是：

• 哥德尔的不完备性定理证明，任何强大到足以表征算术的逻辑系统都将包含在该系统内既不能证明也不能反驳的陈述。 这直接应用于与证明软件完整性和正确性的可行性相关的理论问题。

• 框架问题是使用一阶逻辑表示人工智能代理的目标和状态时必须克服的基本问题。

• Curry-Howard 对应是逻辑系统和软件之间的一种关系。 该理论在证明和程序之间建立了精确的对应关系。 特别是，它表明简单类型 lambda 演算中的项对应于直觉命题逻辑的证明。

• 范畴论代表了一种强调结构之间关系的数学观点。 它与计算机科学的许多方面密切相关：编程语言的类型系统、转换系统理论、编程语言模型和编程语言语义理论。

最早使用人工智能这个术语的应用程序之一是由 Allen Newell、J. C. Shaw 和 Herbert Simon 在 1956 年开发的逻辑理论家系统。 逻辑定律必须为真的结论（附加陈述）。 例如，如果给定一个逻辑系统，声明所有人类都会死，而苏格拉底是人类，那么有效的结论是苏格拉底会死。 当然，这是一个微不足道的例子。 在实际的逻辑系统中，语句可能很多而且很复杂。 人们很早就意识到，这种分析可以通过使用计算机得到显着的帮助。 逻辑理论家验证了伯特兰·罗素和阿尔弗雷德·诺斯·怀特海在他们关于数学逻辑的有影响力的著作《数学原理》中的理论工作。 此外，逻辑学家已经利用后续系统来验证和发现新的逻辑定理和证明。

数理逻辑对人工智能 (AI) 领域的影响一直很大。 从该领域一开始，人们就意识到自动化逻辑推理技术在解决问题和从事实中得出结论方面具有巨大潜力。 Ron Brachman 将一阶逻辑 (FOL) 描述为评估所有 AI 知识表示形式的指标。 没有比 FOL 更通用或更强大的已知方法来描述和分析信息。 FOL 本身不被用作计算机语言的原因是它实际上太具有表现力，从某种意义上说，FOL 可以轻松表达任何计算机（无论多么强大）都无法解决的语句。出于这个原因，每种形式的知识表示在某种意义上都是表达性和可计算性之间的权衡。 语言表达能力越强，越接近FOL，越容易变慢，容易死循环。例如，专家系统中使用的 IF THEN 规则近似于 FOL 的一个非常有限的子集。 出发点不是逻辑运算符的任意公式，而是逻辑学家所说的 modus ponens。 因此，基于规则的系统可以支持高性能计算，特别是如果它们利用优化算法和编译。逻辑理论的另一个主要研究领域是软件工程。 基于知识的软件助手和程序员学徒程序等研究项目应用逻辑理论来验证软件规范的正确性。