人工智能中的自动逻辑推理

人类常用的推理方法不能直接在人工智能中应用从而实现机器的自动推理，本文论述了自动推理中的归结和合一算法的规则和详细步骤，达到使读者容易理解和掌握这一方法的目的，使更多人了解这一方法的作用和前景。

人类思维中严格的推理主要是两种，一种是使用真值表，一种是使用演绎规则。真值表方法，有两个特点，其一，是机械性；其二是，每一个要素，都需要用固定的对象表达出来，假设用n 表示推理中一个命题中含有对象的数目，当n 大到一定程度的时候，2n 会是一个极其庞大的数目，这就限制了它在机器推理当中的应用。

思维中还可以使用演绎推理规则来进行推理， 如常用的分离规则1， 下面两个是利用分离规则的具体例子： 1、如果得了肺炎，那么就会发烧；某人得了肺炎，他一定会发烧。

2、如果得了肺炎，那么，就会出去旅游；某人得了肺炎，所以他会出去旅游。

1 是正确的推理， 2 是错误的推理， 这依赖于人类的经验。

让机器从知识库中， 学会人类的整体经验， 显然存在很大的难度，即使一个库中包含着人类绝大多数经验，检索耗时也限制了其应用。因此这种方法也不适用于机器推理。

归结和合一算法的出现，为解决机器的自动推理提供了很好的方法并得到广泛应用，这一点早已为相关的研究者熟悉。但从事逻辑学研究的人员，往往限于依据罗素和怀特海在《数学原理》中构建的推理体系，不了解机器自动推理的进展。这在人工智能兴起的今天，显然是不满足时代要求的。更多的非专业人士其实也有一窥机器推理的需求，实际工作中，越来越需要构架起《数学原理》中的为人熟知的推理体系与人工智能中自动推理之间的桥梁，让更多的非人工智能领域的研究人员深入认识与了解该方法，这也是本文的主要目的。

1963 年，J. Alan Robinson 找到了在机器上实现逻辑推理的简单方法：著名的归结与合一(resolution and unification)算法[1]。归结原理实质上是一条简洁的推理规则。使用这一条规则，对一阶逻辑中的任一个恒真公式，都将是可证的。到了1972 年，以L. Wos 为代表建立了一个以归结方法为主的自动推理系统。这个系统对于解有限数学、线路设计、程序正确性验证及形式逻辑等领域中的疑难问题，提供了帮助。

1997 年， Leitsch， Alexander 又在The Resolution Calculus 中给出了总结。

至此， 该方法得以广泛应用。

2. 命题逻辑中的归结算法： 令p，q，r，s…表达命题逻辑中的任意一个原子命题，通过命题逻辑的五个连接词¬ ，∨，∧，→， ↔形成合式公式。令A，B，C 为任一合式公式，利用以下规则： (1) 等值式： ()()()ABABBA↔↔→∧→ (2) 蕴析律： ()ABAB→↔¬ ∨ (3) 德·摩根律： ()ABAB¬∨↔¬ ∧¬ 1分离规则是在给定前提A→B,A 都为真时，得到结论B 为真的规则。