( (
z)(z)(
x){[~Q(z)∨P(z)]∧{[Q(x)∧~P(A)]∨[Q(x)∧~P(B)]}}
x){[~Q(z)∨P(z)]∧{Q(x)∧[Q(x)∨~P(B)]∧[~P(A)∨Q(x)]∧[~P(A)∨~P(B)]}
[~Q(z)∨P(z)]∧Q(x)∧[Q(x)∨~P(B)]∧[~P(A)∨Q(x)]∧[~P(A)∨~P(B)] 得子句集: 1, ~Q(z)∨P(z) 2, Q(x2) 3, Q(x3)∨~P(B) 4, ~P(A)∨Q(x4) 5, ~P(A)∨~P(B)
(3)(x)(y){[P(f(x))∧Q(f(B))]→[P(f(A))∧P(y)∧Q(y)]} 目标取反化子句集:
~(x)(y){[P(f(x))∧Q(f(B))]→[P(f(A))∧P(y)∧Q(y)]} ~(x)(y){~[P(f(x))∧Q(f(B))]∨[P(f(A))∧P(y)∧Q(y)]} ( x)( y){[P(f(x))∧Q(f(B))]∧[~P(f(A))∨~P(y)∨~Q(y)]} P(f(x))∧Q(f(B))∧[~P(f(A))∨~P(y)∨~Q(y)] 得子句集: 1,P(f(x1)) 2,Q(f(B))
3,~P(f(A))∨~P(y3)∨~Q(y3)