If we convert
∃u ∀v ∀x ∃y (P(f(u),v, x, y) → Q(u,v,y)) to
∀v ∀x (P(f(a),v, x, g(v,x)) → Q(a,v,g(v,x)))
This process is known as
(A) Simplification (B) Unification
(C) Skolemization (D) Resolution
∃u ∀v ∀x ∃y (P(f(u),v, x, y) → Q(u,v,y)) to
∀v ∀x (P(f(a),v, x, g(v,x)) → Q(a,v,g(v,x)))
This process is known as
(A) Simplification (B) Unification
(C) Skolemization (D) Resolution