例如: Lalx, g(y/y, f(g(b)/zj 就是一个替换,而 ig(n/x, f(x/yb 则不是一个替换,因为x与y出现了循环替换。 定义7设θ={t1/x1,…,tn/xn}是一个替换,E 是一个表达式,把对E施行替换θ,即把E中出现的 个体变元x(1≤m)都用t替换,记为EB,所得 的结果称为E在0下的例( instance)
例如： ｛a/x, g(y)/y ,f(g(b))/z｝ 就是一个替换，而 {g(y)/x, f(x)/y} 则不是一个替换,因为x与y出现了循环替换。 定义7 设θ=｛t1/x1,…,tn/xn｝是一个替换，E 是一个表达式，把对E施行替换θ，即把E中出现的 个体变元xj(1≤j≤n)都用tj替换，记为Eθ，所得 的结果称为E在θ下的例(instance)
定义9设S={F1,F2…,Fn}是一个原子谓词公 式集,若存在一个替换O,可使F10=F20=..=F,O, 则称θ为S的一个合—( Unifier),称S为可合一的。 定义10设σ是原子公式集S的一个合一,如果 对S的任何一个合一日,都存在一个替换λ,使得 0=λ湩 则称σ为S的最一般合( Mostgeneralunifier),简 称MGU
定义9 设S=｛F1 ,F2 ,…,Fn｝是一个原子谓词公 式集，若存在一个替换θ，可使F1θ=F2θ=…=Fnθ， 则称θ为S的一个合一(Unifier)，称S为可合一的。 定义10 设σ是原子公式集S的一个合一，如果 对S的任何一个合一θ，都存在一个替换λ，使得 θ=σ·λ 则称σ为S的最一般合一(MostGeneralUnifier)，简 称MGU
例5.14设S={P(u,y,g(y),P(x,f(u),z) S有一个最一般合 o= fu/x, f(u)/y, g(f(u))/z)Ei 对S的任一合一,例如: 8=a/x, f(a)/y, g(f(a))/z, a/u)ei 存在一个替换 λ={a/u}潼 使得
例5.14 设S=｛P(u,y,g(y)),P(x,f(u),z)｝， S有一个最一般合一 σ=｛u/x,f(u)/y,g(f(u))/z｝ 对S的任一合一，例如： θ=｛a/x,f(a)/y,g(f(a))/z,a/u｝ 存在一个替换 λ=｛a/u｝ 使得 θ=σ·λ
3.2.4谓词逻辑中的归结原理 定义12设C1,C2是两个无相同变元的子 句,L1,L2分别是C1,C2中的两个文字,如果L1和 2有最一般合一0,则子句 (C10-{L10})∪(C2O-{L20})潼称 作C1和C2的二元归结式(二元消解式),C1和C2称 作归结式的亲本子句,L1和L2称作消解文字
3.2.4 谓词逻辑中的归结原理 定义12 设C1,C2是两个无相同变元的子 句，L1,L2分别是C1,C2中的两个文字，如果L1和 L2有最一般合一σ，则子句 (C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝)称 作C1和C2的二元归结式(二元消解式)，C1和C2称 作归结式的亲本子句，L1和L2称作消解文字
例5.18设C1=P(x)∨Q(x),C2=-P(a)∨R(y),求 C1,C2的归结式。 解取L1=P(x),L2==P(a),则L1与一L2的最一般 合-0={a/x},于是, (C10-{L10})∪(C20-{L20}) ({P(a),Q(a)}-{P(a)}) ({-P(a),R(y)}-{-P(a)}) {Q(a),R(y) Q(a)∨R(y)潼 所以,Q(a)VR(y)是C1和C2的二元归结式
例5.18 设C1=P(x)∨Q(x),C2=﹁P(a)∨R(y)，求 C1,C2的归结式。 解 取L1=P(x),L2=﹁P(a),则L1与﹁ L2的最一般 合一σ=｛a/x｝，于是, (C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝) =(｛P(a),Q(a)｝-｛P(a)｝)∪ (｛﹁P(a),R(y)｝-｛﹁P(a)｝) =｛Q(a),R(y)｝ = Q(a)∨R(y) 所以，Q(a)∨R(y)是C1和C2的二元归结式