Is there a unique normal form for each formula of predicate calculus?
I am aware of prenex normal forms of predicate calculus and of disjunctive and conjunctive normal forms of propositional calculus. But what is the name of the combination of the two, i.e. the formula is in prenex normal form and the (quantifier-free) matrix is in - say - disjunctive normal form?
Can uniqueness always be achieved by a optimal choice of variables and sorting and arrangement of the literals of the disjunctive normal form (given that the variables and the relation and function symbols are lexicographically sorted) and elimination of double negation?
Example: The intended unique normal form of
$(\forall x_2) \neg R_2 (x_2) \rightarrow \Big((\exists x_1)\neg\neg R_3(x_1) \wedge R_1(x_1,x_2) \Big)$
should be (not quite sure)
$(\forall x_1)(\exists x_2)\big(R_1 (x_2,x_1) \vee R_2(x_1)\big) \wedge \big( R_2(x_1) \vee R_3 (x_2) \big)$
What is the complexity of finding such normal forms?