例5.19设C1=P(x,y)V_Q(a),C2=Q(x)VR(y), 求C1,C2的归结式。 解由于C1,C2中都含有变元x,y,所以需先对其 中一个进行改名,方可归结(归结过程是显然的,故 从略)。 还需说明的是,如果在参加归结的子句内部含 有可合一的文字,则在进行归结之前,也应对这些 文字进行合一,从而使子句达到最简。例如,设有 两个子句: C=P(x)VP(f(a)∨Q(x) C2=P(y)∨R(b)
例5.19 设C1=P(x,y)∨﹁Q(a),C2=Q(x)∨R(y), 求C1,C2的归结式。 解 由于C1,C2中都含有变元x,y，所以需先对其 中一个进行改名,方可归结（归结过程是显然的，故 从略）。 还需说明的是，如果在参加归结的子句内部含 有可合一的文字，则在进行归结之前，也应对这些 文字进行合一，从而使子句达到最简。例如，设有 两个子句： C1=P(x)∨P(f(a))∨Q(x) C2=P(y)∨R(b)
定义13如果子句C中,两个或两个以上的 文字有一个最一般合一0,则Co称为C的因子, 如果C0是单元子句,则Co称为C的单因子 例5.20设C=P(x)∨P(f(y)∨一Q(x) 令0={f(y)/x},于是 Co=P(f(y)∨-Q(f(y)) 是C的因子
定义13 如果子句C中，两个或两个以上的 文字有一个最一般合一σ，则Cσ称为C的因子， 如果Cσ是单元子句，则Cσ称为C的单因子。 例5.20 设C=P(x)∨P(f(y))∨﹁Q(x), 令σ=｛f(y)/x｝，于是 Cσ=P(f(y))∨﹁Q(f(y)) 是C的因子
定义14子句C1,C2的消解式,是下列二元消 解式之一: (1)C1和C2的二元消解式; (2)C1和C2的因子的二元消解式 (3)C1的因子和C2的二元消解式; (4)C1的因子和C2的因子的二元消解式
定义14 子句C1,C2的消解式，是下列二元消 解式之一： (1) C1和C2的二元消解式; (2) C1和C2的因子的二元消解式; (3) C1的因子和C2的二元消解式; (4) C1的因子和C2的因子的二元消解式
定理4谓词逻辑中的消解式是它的亲本子句 的逻辑结果。 由此定理我们即得谓词逻辑中的推理规则 C1∧C2=>(C10-{L10})U(C20-{L20}) 其中C1,C2是两个无相同变元的子句,L1,L2分别是 C1,C2中的文字,0为L1与L2的最一般合 此规则称为谓词逻辑中的消解原理(或归结原 理)
定理4 谓词逻辑中的消解式是它的亲本子句 的逻辑结果。 由此定理我们即得谓词逻辑中的推理规则： C1∧C2 ＝＞(C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝) 其中C1,C2是两个无相同变元的子句，L1,L2分别是 C1,C2中的文字，σ为L1与L2的最一般合一。 此规则称为谓词逻辑中的消解原理（或归结原 理）
例5.21求证G是A1和A2的逻辑结果。 A1:Vx(P(x)→(Q(x)∧R(x) A2:彐x(P(x)∧S(x) G:彐x(S(x)∧R(x) 证我们用反证法,即证明A1∧A2—G不 可满足。首先求得子句集S:
例5.21 求证G是A1和A2的逻辑结果。 A1: x(P(x)→(Q(x)∧R(x))) A2: x(P(x)∧S(x)) G: x(S(x)∧R(x)) 证 我们用反证法，即证明A1∧A2﹁G不 可满足。首先求得子句集S：