人工智能教程（第2版）第3章.ppt

3.6归结过程的控制策略4．输入归结策略输入归结策略对参加归结的子句有如下限制：参加归结的两个子句中，必须至少有一个子句是初始子句集中的子句。本归结策略是不完备的，也就是说，该子句集S是不可满足的，用该归结原理进行归结时，也不一定能归结出空子句。但是，输入归结策略具有简单高效的优点。5．支持集策略支持集策略对参加归结的子句提出如下限制：每一次归结时，参加归结的两个子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔。可以证明，支持集策略是完备的，即若子句集是不可满足的，则由支持集策略一定可以归结出空子句。3.5归结推理方法3.5.1谓词公式与子句集由于谓词公式千变万化，形形色色，给谓词演算的研究带来一定的困难。为此，先介绍两种谓词演算公式的标准型，也就是范式。一种叫前束形范式，另一种叫斯克林（Skolem）范式。?前束形范式一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域一直延伸到公式之末，同时公式中不出现连接词→及，这种形式的公式称作前束形范式。例如，公式(x)(y)(z)(P(x)∧F(y,z)∧Q(y,z))即是一个前束形的公式。前束形范式的优点在于它的量词全部集中在公式的前面，此部分称作公式的首标，而公式的其余部分实际上是一个命题演算公式。它的缺点是其首标杂乱无章，全称量词和存在量词的排列没有一定的规则。3.5归结推理方法?斯克林范式从前束形范式中消去全部存在量词所得到的公式即为Skolem范式，或称Skolem标准型。Skolem标准型的一般形式是(x1)(x2)…(xn)M(x1,x2,…,xn)其中，M(x1,x2,…,xn)是一个合取范式，称为Skolem标准型的母式。3.5归结推理方法将谓词公式G化为Skolem标准型的步骤如下：（1）消去谓词公式G中的蕴涵（→）和双条件符号（），以～A∨B代替A→B，以(A∧B)∨(～A∧～B)替换AB。（2）减少否定符号（～）的辖域，使否定符号“～”最多只作用到一个谓词上。（3）重新命名变元名，使所有的变元的名字均不同，并且自由变元及约束变元亦不同。（4）消去存在量词。这里分两种情况，一种情况是存在量词不出现在全称量词的辖域内，此时，只要用一个新的个体常量替换该存在量词约束的变元，就可以消去存在量词；另一种情况是，存在量词位于一个或多个全称量词的辖域内，例如，(x1)(x2)…(xn)(y)P(x1,x2,…,xn,y)此时，变元y实际受前面的变元x1，x2，…，xn的约束，需要用Skolem函数f(x1,x2,…,xn)替换y即可将存在量词y消去，得到：(x1)(x2)…(xn)P(x1,x2,…,xn,f(x1,x2,…,xn))（5）把全称量词全部移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。（6）母式化为合取范式：任何母式都可以写成由一些谓词公式和谓词公式否定的析取的有限集组成的合取。3.5归结推理方法例3.8将谓词公式G=(x)((y)P(x,y)→～(y)(Q(x,y)→R(x,y)))化为Skolem标准型。解按照将谓词公式化为Skolem标准型的步骤解题如下：取消“→”和“”连接词。(x)(～(y)P(x,y)∨～(y)(～Q(x,y)∨R(x,y)))把“～”的辖域减少到最多只作用于一个谓词。(x)((y)～P(x,y)∨(y)(Q(x,y)∧～R(x,y)))变量更名。(x)((y)～P(x,y)∨(z)(Q(x,z)∧～R(x,z)))消存在量词。因为存在量词（y）和（z）都在的辖域（x）内，属于上述所讲的第二种情况，所以分别用Skolem函数f(x)和g(x)替换y和z。(x)(～P(x,f(x))∨(Q(x,g(x))∧～R(x,g(x))))全称量词移到左边，由于只有一个全称量词（x），已在左边，所以不移。将母式化为合取范式。(x)((～P(x,f(x))∨Q(x,g(x)))∧(～P(x,f(x))∨～R(x,g(x))))3.5归结推理方法2．子句与子句集定义3.16不含有任何连接词的谓词公式叫原子公式，简称原子，而原子或原子的否定统称文字。定义3.17子句就是由一些文字组成的析取式