resolutioninthepredicatecalculus.ppt

16 谓词演算中的归结 内容提要 合一 谓词演算归结 完备性和可靠性 把任意的合式公式转换成子句集 用归结证明定理 答案抽取 相等谓词 知识 16.1 合一 引入 谓词演算中的归结要比命题演算中的归结棘手得多，因为现在要处理变量。 怎样在{?(?), ??(?)}上归结？其中，?是一个变量，?是不包含?的项。 例如， P(f(y),A)?Q(B,C), ?P(x,A)?R(x,C)?S(A,B)，可以用f(y)置换第二个子句中的x得到?P(f(y),A)?R(f(y),C)?S(A,B)，然后进行归结，得到Q(B,C)?R(f(y),C)?S(A,B)。 合一(Unification) 计算合适的置换的过程。 Cont’d 置换实例(Substitution Instance) 用项置换一个表达式中的变量得到的表达式叫做该表达式的一个置换实例。 例如，P[x,f(y),B]的四个置换实例。 P[z,f(w),B] P[x,f(A),B] P[g(z),f(A),B] P[C,f(A),B] 字母变种(alphabetic variant) 用变量置换变量 基例(ground instance) 没有项包含变量的置换实例。 Cont’d 置换(Substitution) 项、变量对的有限集，s={?1/?1,?2/?2,…,?n/?n}。 变量不能用包含该变量的项置换。例如，{f(x)/x}不是一个合法的置换。 置换的应用 表达式?用置换s得到的置换实例记做?s，通过把置换中的每个变量的每次出现用关联的项替换从原来的表达式?得到。 P[x,f(y),B]{A/y}=P[x,f(A),B] Cont’d 置换的复合 两个置换s1和s2的复合记做s1s2，也是置换，由下面的规则得到 (1)把s2应用到s1的项上； (2)如果s2中的项、变量对中的变量不出现在s1的变量中，则把该项、变量对添加到s1中。 例如，{g(x,y)/z}{A/x,B/y,C/w,D/z}= {g(A,B)/z,A/x,B/y,C/w} Cont’d 置换的性质 (?s1)s2=?(s1s2) (s1s2)s3=s1(s2s3) 例如，?=P(x,y), s1={f(y)/x}, s2={A/y} (?s1)s2=P(f(y),y){A/y}=P(f(A),A) ?(s1s2)=P(x,y){f(A)/x,A/y}=P(f(A),A) 一般，s1s2?s2s1 例如，?(s2s1)=P(x,y){A/y,f(y)/x}=P(f(y),A) Cont’d 表达式集的置换 置换s应用到表达式集{?i}的每一个成员上记做{?i}s，即{?i}s={?is}。 合一置换 表达式集{?i}是可合一的(unifiable)，如果存在一个置换s使得?1s=?2s=?3s=…。这时，s叫做{?i}的一个合一置换(unifier)，因为应用s使得{?i}成为一个单元素集。 例如，{P[x,f(y),B], P[x,f(B),B]}{A/x, B/y}={P[A,f(B),B]} Cont’d 最简合一置换(Most General Unifier，MGU) 一个置换g是表达式集{?i}的最简合一置换，如果对{?i}的任意合一置换s，总是存在置换s，使得{?i}s={?i}gs。 最简合一置换做最少的置换使得表达式相同。 例如，{B/y}是{P[x,f(y),B], P[x,f(B),B]}的一个最简合一置换。 最简合一置换产生的实例出了字母变种之外是唯一的。 Cont’d 例子 w1 w2 MGU P(x) P(A) {A/x} P(f(x),y,g(x)) P(f(x),x,g(x)) {x/y}or{y/x} P(f(x),y,g(y)) P(f(x),z,g(x)) {x/y, x/z} P(x,B,B) P(A,y,z) {A/x,B/y,B/z} P(g(f(v)),g(u)) P(x,x) {g(f(v))/x, f(v)/u} P(x,f(x)) P(x,x) NO MGU! Cont’d 合一算法 列表结构表达式 文字和项写成列表的形式。 例如， ?P(x,f(A,y)) ? (?P x (f A y)) 不一致集(disagreement set) 一个非空的表达式集W的不一致集包含W中由所有表达式第一个不同的符号开始后继符号构成的子表达式。 例如，{(?P x (f A y)), (?P x (f z B))}的不一致集是{A,z}。该不一致集可以用置换{A/z}达到一致。 Cont’d UNIFY(?) 输入：列表结构的表达式集?。 输出：如果?是可合一的，输出?的最简合一置换；否则，输出失败。 1. 初始化： k?0, ?k??