自动推理

在计算机科学中，特别是在知识表示和推理以及金属逻辑中，自动推理领域致力于理解推理的不同方面。对自动推理的研究有助于产生计算机程序，使计算机能够完全或几乎完全自动推理。尽管自动推理被认为是人工智能的一个子领域，但它也与理论计算机科学和哲学有联系。自动推理最发达的子领域是自动定理证明（以及自动化程度较低但更务实的交互式定理证明子领域）和自动证明检查（被视为固定假设下的保证正确推理）。

在使用归纳法和演绎法进行类比推理方面也做了大量的工作。其他重要的课题包括不确定性下的推理和非单调性推理。不确定性领域的一个重要部分是论证，在这个领域中，在更标准的自动演绎的基础上，还应用了最小化和一致性的约束。JohnPollock的OSCAR系统是一个自动论证系统的例子，它比仅仅是一个自动定理检验器更具体。自动推理的工具和技术包括经典逻辑和计算法、模糊逻辑、贝叶斯推理、xxx熵推理和许多不太正式的特别技术。早年形式逻辑的发展在自动推理领域发挥了很大的作用，它本身也导致了人工智能的发展。形式证明是一种证明，其中每一个逻辑推理都被检查到数学的基本公理。所有的中间逻辑步骤都被提供，没有例外。