人工智能确定性推理.ppt

4.4.4 用归结反演求取问题的答案（4/4） ﹁At(li,v)∨At(li,v) ﹁C(x, y)∨﹁At(x, u)∨At(y, u) At(li,v)∨﹁ C(x, li)∨﹁At(x, v) C(zhang, li) ﹁ At(zhang,v)∨At(li, v) At(zhang, 302) At(li, 302) {li/y,v/u} {Zhang/x} {302/v} 4.4.2 鲁滨逊归结原理3. 谓词逻辑的归结（4/16） 例4.13 设C1=P(x)∨﹁Q(b)，C2=﹁P(a)∨Q(y)∨R(z) 解：对C1和C2通过最一般合一（σ={a/x, b/y}）的作用，可以得到两个互补对。 注意：求归结式不能同时消去两个互补对，这样的结果不是二元归结式。如在σ={a/x, b/y}下，若同时消去两个互补对，所得的R(z)不是C1和C2的二元归结式。 例4.14 设C1=P(x)∨P(f(a))∨Q(x) ，C2=﹁P(y)∨R(b)，求C12 解：对参加归结的某个子句，若其内部有可合一的文字，则在进行归结之前应先对这些文字进行合一。本例的C1中有可合一的文字P(x)与P(f(a))，若用它们的最一般合一σ={f(a)/x}进行代换，可得到 C1σ=P(f(a))∨Q(f(a)) 此时可对C1σ与C2进行归结。选L1= P(f(a)), L2 =﹁P(y)，L1和L2的最一般合一是σ={f(a)/y}，则可得到C1和C2的二元归结式为 C12=R(b)∨Q(f(a)) 我们把C1σ称为C1的因子。一般来说，若子句C中有两个或两个以上的文字具有最一般合一σ，则称Cσ为子句C的因子。如果Cσ是一个单文字，则称它为C的单元因子。 应用因子概念，可对谓词逻辑中的归结原理给出如下定义： 4.4.2 鲁滨逊归结原理3. 谓词逻辑的归结（5/16） 定义4.21若C1和C2是无公共变元的子句，则 ① C1和C2的二元归结式; ② C1和C2的因子C2σ2的二元归结式； ③ C1的因子C1σ1和C2的二元归结式； ④ C1的因子C1σ1和C2的因子C2σ2的二元归结式。 这四种二元归结式都是子句C1和C2的二元归结式，记为C12。 例4.15 设C1=P(y)∨P(f(x))∨Q(g(x)) ，C2=﹁P(f(g(a)))∨Q(b)，求C12。 解：对C1 ，取最一般合一σ={f(x)/y}，得C1的因子 C1σ=P(f(x))∨Q(g(x)) 对C1的因子和C2归结（σ={g(a)/x }），可得到C1和C2的二元归结式 C12=Q(g(g(a)))∨Q(b) 说明： 对谓词逻辑，定理3.2仍然适用，即归结式C12是其亲本子句C1和C2的逻辑结论。用归结式取代它在子句集S中的亲本子句，所得到的子句集仍然保持着原子句集S的不可满足性。 此外，对谓词逻辑定理3.3也仍然适用，即从不可满足的意义上说，一阶谓词逻辑的归结原理也是完备的 4.4.2 鲁滨逊归结原理3. 谓词逻辑的归结（6/16） 谓词逻辑的归结反演 谓词逻辑的归结反演过程与命题逻辑的归结反演过程相比，其步骤基本相同，但每步的处理对象不同。例如，在步骤(3)化简子句集时，谓词逻辑需要把由谓词构成的公式集化为子句集；在步骤(4)按归结原理进行归结时，谓词逻辑的归结原理需要考虑两个亲本子句的最一般合一。 例4.16 已知 F: (?x)((?y)(A(x, y)∧B(y))→(?y)(C(y)∧D(x, y))) G: ﹁(?x)C(x)→(?x)(?y)(A(x, y)→﹁B(y)) 求证G是F的逻辑结论。 证明：先把G否定，并放入F中，得到的{F, ﹁G}为 {(? x)((? y)(A(x,y)∧B(y))→(? y)(C(y)∧D(x,y))), ﹁(﹁(? x)C(x)→(? x)(? y)(A(x,y)→﹁ B(y)))} 4.4.2 鲁滨逊归结原理3. 谓词逻辑的归结（7/16） 再把{F,﹁G}化成子句集，得到 (1) ﹁A(x,y)∨﹁ B(y) ∨C(f(x)) (2) ﹁ A(u,v)∨﹁ B(v) ∨D(u,f(u)) (3) ﹁ C(z) (4) A(m,n) (5) B(k) 其中，(1)、(2)是由F 化出的