自动推理
自动推理是（英语：automated reasoning），计算机科学和数理逻辑的一个交叉领域，致力于了解理智的方方面面。自动逻辑的研究帮助了利用计算机自动进行完全或几乎完全的推理，其内容一般可分为演绎推理和非演绎推理。自动推理被认为是人工智能的一个分支，还和理论计算机科学甚至哲学相关联。
自动推理的研究内容包括定理机器证明、证明自动检查（Automated_proof_checking）、不确定性推理、非单调逻辑以及类比归纳和外展推理。自动推理的技术和工具包括经典逻辑、微积分学、模糊逻辑、贝叶斯推断、推理与最大熵和大量的非正式特别技术。
在20世纪60年代中期以前，定理机器证明的注意力还仅仅限于数学方面。从60年代后期，开始将注意力转向数学以外的其他领域，如程序自动生成、逻辑程序设计以及更一般的智能系统中的推理问题。定理机器证明的研究是自动推理领域中的先驱性工作。70年代专家系统和知识工程的出现，使人们认识到，仅仅研究从真前提得出真结果的古典推理方法是不够的，因为人类面对的是一个充满不确定信息的环境，人类在这种环境里进行着有效的思考和推理。为了建立类似于人的智能系统，研究更接近人类思维方式的推理，如非单调推理、模糊推理等，变得越来越必要。
自动推理的研究，一方面表现在专家系统中，各种面向特殊问题的推理方式的研究，例如，DENDRAL的用于化学合成的推理，PROSPECTOR的用于地质方面的推理，MYCIN的用于医疗诊断的推理等；另一方面，在计算机辅助推理的研究上也取得成果，回答了以前在数学和形式逻辑方面的一些未解问题。随之而来的，面向自动推理的逻辑程序设计语言（如PROLOG）也引起了研究者的兴趣。
自动推理的研究内容有模型生成与定理机器证明、程序正确性验证、逻辑程序设计、常识推理、非单调推理、模糊推理、约束推理、定性推理、类比推理、归纳推理、自然演绎法、归结方法、重写方法、吴方法等。
自动推理的近期目标是得到各种推理程序，它们中的每一个都相当于一个自动推理助手，人们能有效地和这个助手“交谈”。远期目标是当你向这样一个程序提出问题后，你就可以去考虑别的问题了；当你再回来时，原来的问题已经解决了。
参见
