数据词典：自动推理（Automated Reasoning）

赵老师

自动推理(automated reasoning)是在计算机支持下实现推理，求解问题。它是人工智能领域中的重要研究课题。在20世纪60年代中期以前，定理机器证明的注意力还仅仅限于数学方面。从60年代后期开始，定理机器证明领域的研究者已开始将注意力转向数学以外的其它领域，诸如程序自动生成、逻辑程序设计以及更一般的智能系统中的推理问题。

定理机器证明的研究是自动推理领域中的先驱性工作。70 年代专家系统和知识工程的出现，使人们认识到，仅仅研究从真前提得出真结果的古典推理方法是不够的。因为人类面对的是一个充满不确定信息的环境。人类在这种环境里进行着有效的思考和推理。因此，为了建立类似于人的智能系统，研究那些更接近人类思维方式的推理，例如，非单调推理、模糊推理等等，就变得越来越必要了。

目前自动推理的研究，一方面，表现在专家系统中，各种面向特殊问题的推理方式的研究，例如，DENDRAL系统的用于化学合成的推理，PROSPECTOR的用于地质方面的推理，MYCIN的用于医疗诊断的推理等等；另一方面，在计算机辅助推理的研究上，也取得成果。例如, 以L . Wos为首的小组在美国Argonne国家实验室建立的AURA系统，这个系统已经帮助人们回答了以前在数学和形式逻辑方面的一些未解问题。随之而来的面向自动推理的程序语言，如PROLOG，也引起了研究者的兴趣。

自动推理领域的研究还是初步的，诸如领域知识的表示，推理规则的控制策略等重要问题，都没有满意的解决。一个明显的例子是：人能进行迅速推理的很多问题，用自动推理程序时，仍要花费大量时间。推理程序和人之间的通信仍很困难，自然语言处理方面的工作和自动推理的进展有重要关系。L . Wos 认为解决自动推理的关键是利用现在和将来的推理程序对已经解决和尚未解决的问题进行实验，从而导致新的推理规则和有效策略的发现。例如， 对数论问题求解的尝试，导致L . Wos 发现了调解方法。

自动推理包含下面一些研究内容：定理机器证明、程序正确性验证、程序自动生成、逻辑程序设计、非单调推理、模糊推理、约束推理、定性推理、类比推理、归纳推理、自然演绎法、归结方法、重写方法等等。

自动推理的近期目标是：得到各种推理程序，它们中的每一个都相当于一个自动推理助手，人们应该能有效地和这个助手“交谈”。远期目标应该是：当你向这样一个程序提出问题后，你就可以去考虑别的问题了；当你再回来时，原来的问题已经解决了，丝毫没有你的帮助和干涉。

日本在执行其五代机研制的十年计划中得到如下一个看法：新一代计算机应该是一种新概念下的计算机。它的机器语言应该是像PROLOG 语言那样的谓词逻辑符号串。用逻辑表示信息，用逻辑推理解决问题将是新一代计算机的特征。因此，这种计算机的基本操作不再是算术运算，而是逻辑推理。所以，自动推理的研究，对于未来一代新型计算机的设计是很有必要的。

【出处】张效祥. 计算机科学技术百科全书,清华大学出版社,2018年5月第3版.