(4)(x)(
y)P(x,y)→(
y)(x)P(x,y)
目标取反化子句集: ~{(x)( ~{~[(
x)( ~{~[(
x)( [(x)( (x)(
y)P(x,
y)→(
y)(x)P(x,y)} y)(x)P(x,y)} v)(u)P(u,v)} u)~P(u,v)
y)P(x,y)]∨(y)P(x,y)]∨(
y)P(x,y)]∧(v)(y)(v)(
u)P(x,y)]∧~P(u,v)
P(a,y)∧~P(u,f(y)) 得子句集: 1,P(a,y1) 2,~P(u,f(y2))
(5)(x){P(x)∧[Q(A)∨Q(B)]}→(x)[P(x)∧Q(x)]
目标取反化子句集: ~{(
x){P(x)∧[Q(A)∨Q(B)]}→(x)[P(x)∧Q(x)]}
~{~{(x)P(x)∧[Q(A)∨Q(B)]}∨(x)[P(x)∧Q(x)]} {( {( (
x)P(x)∧[Q(A)∨Q(B)]}∧(x)P(x)∧[Q(A)∨Q(B)]}∧(x)(
x)[~P(x)∨~Q(x)]} y)[~P(y)∨~Q(y)]}
y){P(x)∧[Q(A)∨Q(B)]∧[~P(y)∨~Q(y)]}
P(x)∧[Q(A)∨Q(B)]∧[~P(y)∨~Q(y)] 得子句集: 1,P(x)