人工智能基础（第2版）-高济-AI-6-本.pptVIP

人工智能基础 浙江大学计算机学院 高 济 3 归结原理 动机 尽管海伯伦提出的H域（即海伯伦域）和海伯伦定理，为自动定理证明奠定了理论基础；但并未提供有效的操作化方法。 为提高判定子句集不可满足的有效性，鲁宾逊于1965年提出了归结(Resolution)原理，也称为消解原理。归结原理简单易行，便于计算机实现和执行，从而使定理的机器自动证明成为现实，也成为人工智能技术实用化的一次重要突破。 基本思路 是通过归结方法不断扩充待判定的子句集，并设法使其包含进指示矛盾的空子句。空子句是不可满足（即永假）的子句，既然子句集中子句间隐含着合取关系，空子句的出现实际上判定了子句集不可满足。 3 归结原理 1）归结方法 归结式C = C1’∨C2’， 由二个子句 C1 = L∨C1’, C2 = ? L∨C2’ 归结而成， 从C1 和C2 中消去互补文字L和? L，并通过析取将C1 和C2 的剩余部分组成新的子句， 例子：P(A)∨Q(x)∨R(f(x)), ? P(A)∨Q(y)∨R(y)的归结式： Q(x)∨R(f(x))∨Q(y)∨R(y)。 归结式性质： 定理：二个子句C1 和C2 的归结式C是C1 和C2 的逻辑推论。 推论：设C1 和C2 是子句集S中的两个子句，并以C作为它们的归结式，则通过往S中加入C而产生的扩展子句集S’与子句集S在不可满足的意义上是等价的，即：S’的不可满足? S的不可满足。 空子句C = 口 由C1 = L和C2 = ? L归结而成， 空子句是不可满足的子句，指示C1 和C2 是一对矛盾子句，成为用归结原理判定子句集不可满足的成功标志。 3 归结原理 2）归结推理过程 命题逻辑中的归结推理过程： 子句中文字只是原子命题公式或其 取反， 不带变量，易于判别哪些子句对包 含互补文字， 归结过程表示为归结演绎树， 例子：S={?P∨Q, P∨R, ?Q, ?R} (图2.24) 谓词逻辑中的归结推理过程： 子句中含有变量，不能直接发现和消去互补文字， 需对潜在的互补文字先作变量置换和合一处理。 2）归结推理过程 变量置换——用置换项取代公式中的变量，置换项可以是变量、常量或函数。 置换——包含若干置换元素（形如t/v）的集合， t/v ——置换项/变量。 例子 潜在的互补文字：P(x, y, x, g(x)), ?P(A, B, A, z) 置换：S1 = {A/x, B/y, g(x)/z} S2 = {f(w)/x, z/y, C/z} S3 = {B/x, f(w)/y, y/z} 置换结果：{P(x, y, x, g(x)), ?P(A, B, A, z)}S1 ={P(A, B, A, g(A)), ?P(A, B, A, g(A))} {P(x, y, x, g(x)), ?P(A, B, A, z)}S2 ={P(f(w)), z, f(w), g(f(w)), ?P(A, B, A, C)} {P(x, y, x, g(x)), ?P(A, B, A, z)}S3 ={P(B, f(w), B, g(B)), ?P(A, B, A, y)} 2）归结推理过程 潜在互补文字的合一处理——通过变量置换，使相应于这二个文字的原子谓词公式同一化的过程。 健全的合一算法——面向任意表达式， 归结演绎过程中只须对原子谓词公式作合一处理， 只需通过一个匹配过程去检查两个原子谓词公式的可合一性，并同时建立用于实现合一的置换。 匹配过程： 例子： P(x, y, x, g(x)), P(A, B, A, z) 可合一，实现合一的置换S1={A/x, B/y, g(x)/z}。 2）归结推理过程 谓词逻辑中子句归结例： C1 = P(x, y)∨Q(x, f(x))∨R(x, f(y)) C2 = ?P(A, B)∨?Q(z, f(z))∨R(z, g(z)) 令L11 = P(x, y), L21 = ?P(A, B), L11和?L21可合一 L11和L21是互补文字 置换S1 = {A/x, B/y} 变量的置换必须在整个子句对范围内进行 归结式：Q(A, f(A))∨R(A, f(B))∨?Q(z, f(z))∨R(z, g(z)) 两个子句可以有多于一对的互补文字， 另一对互补文字：L12 = Q(x, f(x)), L22 = ?Q(z, f(z)) 置换S2 = {z/x} 归结式： P