一阶谓词逻辑归结原理 gaunthan Posted on Nov 12 2016 ? Artificial Intelligence ? ? Auto-Reasoning ? > 阅读本文前请先阅读[《推理方法之归结推理法》](http://blog.leanote.com/post/gaunthan/AI-%E6%8E%A8%E7%90%86%E6%96%B9%E6%B3%95%E4%B9%8B%E5%BD%92%E7%BB%93%E6%8E%A8%E7%90%86%E6%B3%95)，以获得一定理论基础。 ## 概述 谓词逻辑的归结方法和命题逻辑的归结方法的基本原理是一样的。由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以在生成子句集之前要对逻辑公式做一些处理，将其转化为**Skolem标准型**，然后在**子句集**的基础再进行归结，其中还要涉及**置换和合一**。因此，虽然基本的方法相同，但是归结过程较之命题公式的归结过程要复杂得多。 ## Skolem标准型 为了能够像命题逻辑计算那样进行归结，首先必须解决谓词逻辑中的量词问题。具体的解决方法请阅读文章[《Skolem标准型》](http://blog.leanote.com/post/gaunthan/%E7%A6%BB%E6%95%A3%E6%95%B0%E5%AD%A6-Skolem%E6%A0%87%E5%87%86%E5%9E%8B)。 ## 子句集 ### 定义 同命题逻辑的归结方法一样，在应用谓词归结原理推理之前，首先要将待证明的定理的谓词公式集合转换成为谓词子句的集合。为了描述子句集，需要知道以下名词定义： - **文字**：不含任何连接词的谓词公式。 - **子句**：一些文字的析取（谓词的和）。不含任何文件的子句称为空子句，记为“$\square$”。 - **子句集**：所有子句的集合。 ### 转换过程 对于任一个谓词公式$G$，都可以通过Skolem标准型，标准化建立起一个子句集与之想对应。因为子句不过是一些文字的析取，是一种比较简单的形式，所以对$G$的讨论用对子句集$S$的讨论来代替，更加容易处理。 子句集$S$的求取过程： 1. 将谓词公式$G$转换为前束范式； 2. 消去前束范式中的存在量词，略去其中的任意量词，生成Skolem标准型； 3. 将Skolem标准型中的各个子句提出，表示为集合形式。 可以简单地把求取过程理解为： > 用“,”取代Skolem标准型中的“$\land$”，并表示为集合形式。 例如，$P(a, x, f(x)) \land \lnot Q(g(x), b) \land \lnot R(x)$的子句集为： $$\lbrace P(a, x, f(x)), \lnot Q(g(x), b), \lnot R(x) \rbrace $$ ## 置换 置换可以简单地理解为是在一个谓词公式中用置换项去置换变量。 置换是形如$\lbrace t_1/x_1, t_2/x_2, ···, t_n/x_n \rbrace $的有限集合，其中$x_1, x_2, ···, x_n$是互不相同的变量，即置换变量；$t_1, t_2, ···, t_n$是不同于$x_i$的项（常量、变量、函数），即置换项；$t_i/x_i$表示用$t_i$置换$x_i$，并且要求$t_i$与$x_i$不能相同，而且$x_i$不能循环地出现在另一个$t_i$中。注意，这里$t_i/x_i$的意思是说用$t_i$置换在整个置换区域范围内的所有$x_i$，每一次出现都要置换。 ### 置换的合成 设$\theta = \lbrace t_1/x_1, t_2/x_2, ···, t_n/x_n \rbrace$和$\lambda = \lbrace u_1/y_1, u_2/y_2, ···, u_n/y_n \rbrace$是两个置换，则$\theta$与$\lambda$的合成也是一个置换，记作$\theta \bullet \lambda$。它是集合 $$\lbrace t_1 \bullet \lambda/x_1, t_2 \bullet \lambda/x_2, ···, t_n \bullet \lambda/x_n, u_1/y_1, u_2/y_2, ···, u_n/y_n \rbrace$$ 即对$t_i$先做$\lambda$置换；然后再做$\theta$置换，置换$x_i$。其中删去了以下两种元素： - $t_i\lambda = x_i$时，删去$t_i\lambda/x_i(i = 1, 2, ···, n)$； - 当$y_i \in \lbrace x_1, x_2, ···, x_n \rbrace$时，删去$u_j/y_j(j = 1, 2, ···, m)$ 最后剩下的元素构成新的置换集合。 ### 置换的性质 - 结合律。满足$(\theta \bullet \lambda_1)\lambda_2 = \theta(\lambda_1 \bullet \lambda_2)$和$\theta (\lambda_1 \bullet \lambda_2) = (\theta \bullet \lambda_1) \lambda_2$。 - 交换律（不成立）。一般来讲，置换的合成不满足交换律，即$\lambda_1 \bullet \lambda_2 \neq \lambda_2 \bullet \lambda_1$。 ## 合一 合一可以简单地理解为：寻找相对变量的置换，使两个谓词公式一致。 设有公式集$F = \lbrace F_1, F_2, ···, F_n \rbrace$，若存在一个置换$\theta$，可使$F_1\theta = F_2\theta = ··· = F_n\theta$，则称$\theta$是$F$的一个合一，同时称$F_1, F_2, ···, F_n$是可合一的。 一般来说，一个公式集的合一不是唯一的。 ### 最一般合一 设$\sigma$是谓词公式集$F$的一个合一，如果对$F$的任意一个合一$\sigma$都存在一个置换$\lambda$，使得$\theta = \sigma \bullet \lambda$，则称$\sigma$是一个**最一般合一**(most general unifier, mgu)。 ### 求取最一般合一 对于给定的两个公式，采用逐一比较找出不一致，并作相应的合一置换，则可求得最一般合一置换。 ## 归结过程控制策略 - 要解决的问题是归结方法的知识爆炸； - 控制策略的目的是归结点尽量少； - 控制策略的原则是删除不必要的子句，或对参加归结的子句加以限制； - 给出控制策略，以便仅选择合适的子句对其做归结，避免多余的、不必要的归结式出现。 ### 删除策略 在归结过程总随时删除以下子句： - 含有永真式的子句； - 被子句集中其他子句归类的子句。 ### 使用支撑集策略 每一次参加归结的亲本子句中，应该有一个是有目标公式的否定所得到的子句或者它们的后裔。 赏 Wechat Pay Alipay DNS 服务器 Skolem标准型
