第3章谓词逻辑和归结原理

第3章谓词逻辑和归结原理内容摘要：

的变量可以在量词作用范围内用另外变量代替。 我们可以对变量适当地改名 , 使每一个量词所约束的变量都有不同的名字 . 例如 , 谓词公式 （ x） P（ x） ∨ (x) Q（ x） 改写成 （ x） P（ x） ∨ (y )Q（ y） . 4. 删除公式中的存在量词 . 例如 ,谓词公式 （ x)(y)P（ x, y) 在删去存在量词之后 , 变成 （ x)P（ x, f(x)) , 在删去存在量词之后 , 这个存在量词所约束的变量的每次出现都用一个函数代替 , 这个函数的自变量是约束范围包含删除的存在量词的所有全称量词限制的变量 . 这个函数也叫做 Skolem函数 . 把删除存在量词 ,将存在量词限制的变量用对应的 Skolem函数代替的过程叫做 Skolem化过程 . 结果叫做 Skolem范式 . )]()()()[~( xQxxPx 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 例 将下式化为 Skolem标准型 : ～ (（ x) (y )P(a,x,y) → ( x )( ～（ y） Q(y,b) →R(x))) ～ (～ （ x) (y )P(a,x,y) ∨ ( x )( ～ ～ （ y） Q(y,b) ∨ R(x))) （ x) (y )P(a,x,y) ∧ ～ (x )(（ y） Q(y,b) ∨ R(x))) （ x) (y )P(a,x,y) ∧ (  x )(（  y） ～ Q(y,b) ∧ ～ R(x))) （ x) ((y )P(a,x,y) ∧ ( （  y） ～ Q(y,b) ∧ ～ R(x))) （ x) ((y )P(a,x,y) ∧ ( （  z） ～ Q(z,b) ∧ ～ R(x))) （ x) (y ) （  z） ( P(a,x,y) ∧ ～ Q(z,b) ∧ ～ R(x)) （ x) （  z） ( P(a,x,f(x)) ∧ ～ Q(z,b) ∧ ～ R(x)) （ x) ( P(a,x,f(x)) ∧ ～ Q(g(x),b) ∧ ～ R(x)) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (子句集 ) 文字 我们把命题原子称作正文字， 例如 P(x), Q(y,b), R(w,c)„., 等等， 把带有非符号的命题原子叫做负文字，例如 ~P(y), ~Q(a,b), ~R(x,y,z)„., 等等，把正文字和负文字统称为文字。 子句 单个文字， 文字的析取构成的命题逻辑公式叫做子句。 例如， P, ~Q(x) , P(x) ∨ ~ Q(y,b), 都是子句。 子句集 若干子句的集合 . 一个命题逻辑公式可以采用如下方式转换成等价的子句的合取形式 , 即合取范式： 1. 利用等价公式 P←→ Q =( P→Q)∧ (Q←P) 和 P→Q=~P∨Q删去公式中的 ←→ 符号和 → 符号 . 2. 利用 De Man 律把所有的否定符号移到每个原子之前 . 3. 利用分配律得到子句的合取形式 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (子句集 ) 4. 把公式变换成 Skolem标准型 . 5. 把 Skolem标准型中子句提出 .表示为集合形式 . 定理 公式 G是不可满足的 , 当且仅当其子句集 S是不可满足的 , 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 在命题逻辑归结中 , 需要两个子句有互补文字 , 这两个文字除了否定符号之外是完全相同的 . 但在谓词逻辑中包含变量 , 而变量可以指定成其他任何常量 , 变量 , 或者函数项 , 可以在指定后再实施归结 , 因此即使两个项不完全相同 , 也可能进行归结 . 例如 , 设有谓词逻辑子句 c1和 c2 ， c1=P(x)∨ ~ Q(x,y) c2= ~ P(f(a))∨ R(x,b), 表明上看来没有互补文字 , 但是 , 如果把 c1和 c2中的 x都指定成 f(a), 则有互补对 P(f(a)) 和 ~ P(f(a)), 这时 c1和 c2 就可以归结得到 ~ Q(f(a),y)∨R(f(a),b), 这种为变量的指定称为替换 , 本节我们先介绍替换 . 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 替换是如下形式的偶对组成的集合 : s = { t1/ v1, t2/ v2,…, tn/ vn, } 其中 t1, t2,…, tn 是项 , v1, v2,…, vn 是彼此不同的变量 , ti中不包含变量 vi. 例如 , 下面的 4个偶对集合是 4个替换 : s1 = {z/x, w/y} s2 = {A /y} s3 = {g(z)/x, A/y} s4 = {C/x, A/y} 把替换 s用于表达式 E是把 E中变量 vi的每次出现都用对应的项 ti 代替 (i =1,2,…, n ), 成为表达式 E的替换例，记为 Es. 例如， 设 E = P(x, f(y), B), 则 Es1 = P(z, f(w), B) Es2 = P(x, f(A), B) Es3 = P(g(z), f(A), B) Es4 = P(C, f(A), B) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 设 s1和 s2 是两个替换， s1= { t1/ x1, t2/ x2,„, tn/ xn } s2 = {u1/ y1, u2/ y2,„, un/ yn } 我们可以利用 s1和 s2组合产生一个新的替换， 这种组合相当于引进替换中的一种运算， 记为 s1s2, 其结果是把 s2用在 s1的所有的项 ti 上 (i =1,2,„, n ) ， 然后把 s2中加进去， 得到 { t1s2/ x1, t2s2/ x2,…, tns2/ xn, u1/ y1, u2/ y2,…, um/ ym} 再删除一些不符合替换要求的偶对 :tis2=xi, s2变量在 s1出现的偶对。 例如， 设： s1= { f(y)/ x , z/y}, s2 = { a/ x, b/ y, y/ z } 则 从集合中 { f(b)/ x , y/y, a/ x, b/ y, y/ z } 删除 y/y， a/ x， b/ y,得到 s1s2={ f(b)/ x , y/ z } 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 替换的复合运算满足结合律， 不满足交换律。 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 设 {E1, E2, „, En} 是一个表达式集合，如果存在一个替换 s，把 s用于这个表达式集合的替换例集合满足 E1s = E2s= ,„,= Ens, 则称该表达式集合是可合一的， 而 s称为该表达式集合的合一替换。 例如， 设 E1=P(x, f(y),B), E2=P(x, f(B),B), s={ A/ x, B/ y}, 则容易验证 E1s = E2s= P(A, f(B),B) 因此 E1和 E2是可合一的。 尽管这个替换 s可以使 E1和 E2合一， 但 s并不是最简单的。 在谓词逻辑归结中， 我们总希望使用最简单的合一。 因此下面给出最一般合一的概念。 设设 {E1, E2, „, En} 是一个表达式集合， g是该表达式集合的一个合一替换 , 如果对任何合一替换 s, 都有替换 s’, 满足 s = gs’ ， 则称 g是 {E1, E2, „, En} 的最一般合一替换。 在我们上述的例子中，最一般合一替换是个 g={ B/ y}, s = g {A/x}. 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 求最一般合一算法 1. 令 W={F1, F2} 2. 令 k=0, W0=W, s0={} 3. 如果 Wk已合一 , 停止 , sk=mgu, 否则 , 找不一致集合 Dk, 4. 如果 Dk中存在元素 vk和 tk, 并且 vk不出现在 tk中 , 转 5, 否则不可合一 . 5. sk+1=sk{tk/vk}, Wk+1=Wk{tk/vk} 6, k=k+1, 转 3. 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (替换与合一 ) 例 , 设 f1=P(a,x,f(g(y))), F2=P(z, f(a), f(u)) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结式 ) 谓词逻辑归结式 设 c1, c2是两个子句， 为叙述方便， 我们假定子句都写成文字集合的形式， 而把这些集合中文字的关系约定为析取。 c1={L1}∪ D1, c2={~L2}∪ D2 , 其中 L1 ， L2是可合一的原子， 假设它们的最一般合一是 s， D1和 D2 为子句． 则 c1, c2的归结式 r 为： [(c1 ―{L1 }) ∪ (c2―{~L2})] s 在对子句实施归结之前， 为了避免不必要的混淆，我们对子句中的变量进行改名， 使得各子句中的变量都使用不同的名字。 例如， 假设我们想要对两个子句 P(x) ∨ Q(f(x)) 和 R(g(x)) ∨ ~ Q(f(A))实施归结， 我们先把第二个子句中变量进行改名， 得到 R(g(y)) ∨ ~ Q(f(A)), 然后通过归结得到 P(A) ∨ R(g(y)), 这种变量改名的过程也叫做变量的分离标准化。 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结式 ) 例 (1) c1= P(x) ∨ Q(x,y) 和 c2=~ P(a) ∨ ~ R(b, z) 它们的归结式 R(c1, c2)= Q(a,y) ∨ ~ R(b, z) 例 (2) c1= P(x, y) ∨ Q(x) ∨ R(x) 和 c2=~ P(a, z) ∨ ~ Q(b) 它们的归结式 R(c1, c2)= Q(a) ∨ R(a) ∨ ~ Q(b) 或者 P(b, y) ∨ R(b) ∨ ~ P(a, z) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结过程 ) 谓词逻辑中归结方法的主要思想与命题逻辑相同。 假设我们想从公式集合 SF = {f1, „ , fn} 出发证明公式 g, SF称为前提集合， g称为结论，我们先把 f1, „ , fn 和  g 转换成子句集 Cf1, „ , Cfn 和 Cg, 设 SC = Cf1  , „ ,  Cfn  Cg 为初始子句集，然后在 SC的子句间实施归结，不断地加入新的归结式，然后继续归结，当子句集中出现了空子句时， 我们就证明了 SF  g, 即证明了 g是 SF的逻辑结果。 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结过程 ) 例 假设任何任何通过计算机考试并获奖的人都是快乐的， 任何肯学习或幸运的人都可以通过所有的考试， 张不肯学习但他是幸运的， 任何幸运的人都能获奖。 求证： 张是快乐的。 R1:任何任何通过计算机考试并获奖的人都是快乐的 （ x)((Pass(x, puter) ∧ Win(x, prize)) →Happy(x)) R2:任何肯学习或幸运的人都可以通过所有的考试， （ x) （ y) ((Study(x) ∨ Lucky(x)→ )((Pass(x, y)) R3:张不肯学习但他是幸运的 ~Study(zhang) ∧ Lucky(zhang) R4:任何幸运的人都能获奖 （ x) (Lucky(x)→ Win(x, prize)) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结过程 ) 要证的结果：张是快乐的。 Happy(zhang) 转换为子句 1. ~ Pass(x, puter) ∨ ~ Win(x, prize)) ∨ Happy(x)) 2. ~ Study(y) ∨ Pass(y, z) 3. ~ Lucky(u) ∨ Pass(u, v) 4. ~Study (zhang) 5. Lucky(zhang) 6. ~ Lucky(x) ∨ Win(x, prize) 7. ~ Happy(zhang) 吉林大学珠海学院计算机科学与技术系 人工智能 谓词归结原理 (归结过程 ) 8. ~ Pass(w, puter) ∨ Happy(w))∨ ~ Lucky(w) 1,6 {w/x} 9.。