I want to transform an arbitrary formula of first-order logic into a CNF, or rather into a Skolem formula, whose matrix is in CNF. Standard procedure: First skolemize (the prenexed formula), then bring matrix into negation normal form and last distribute conjunctions and disjunctions appropriately. The last step however may lead to an exponential blow-up of my formula size.
I was thinking about using the Tseitin-Transformation. For this I would not introduce new propositional variables at the left-hand side of the biconditionals to the subformulas in my matrix, but rather use new predicate symbols which are applied to those variables occurring in the formula for which the new literal should stand, e.g. for a subformula of the matrix: $$P(x,y) \land Q(x)$$ I would introduce a predicate symbol new to my formula, say $R$ thus having $$R(x,y) \leftrightarrow P(x,y) \land Q(x)$$ Afterwards I would then proceed as in the propositional case.
Is this approach correct in that it yields an equisatisfiable formulain the case of first-oder logic? Thank you!